projects / coq-hetmet.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 97552c1) | patch
fix proof that Judgments(L) is Cartesian
authorAdam Megacz <megacz@cs.berkeley.edu>
Sat, 26 Mar 2011 02:18:09 +0000 (19:18 -0700)
committerAdam Megacz <megacz@cs.berkeley.edu>
Sat, 26 Mar 2011 02:18:09 +0000 (19:18 -0700)
commit8cb97991a95d5761a28ca94767b8fe637d1411d9
treeb6c66bb2a56dab80f074ee11368a2d30a4f9581atree | snapshot
parent97552c1a6dfb32098d4491951929ab1d4aca96a0commit | diff
fix proof that Judgments(L) is Cartesian
src/NaturalDeduction.v diff | blob | history
src/NaturalDeductionCategory.v diff | blob | history
src/ProgrammingLanguage.v diff | blob | history
src/categories diff | blob | history
Coq proofs and code accompanying the HetMet extensions for GHC