summary |
shortlog | log |
commit |
commitdiff |
tree
first ⋅ prev ⋅ next
Adam Megacz [Mon, 7 Mar 2011 13:41:56 +0000 (05:41 -0800)]
add HaskProofToStrong skeleton implementation
Adam Megacz [Mon, 7 Mar 2011 13:41:54 +0000 (05:41 -0800)]
add HaskStrongToWeak
Adam Megacz [Mon, 7 Mar 2011 13:41:51 +0000 (05:41 -0800)]
add HaskStrongToProof
Adam Megacz [Mon, 7 Mar 2011 13:41:48 +0000 (05:41 -0800)]
add HaskWeakToStrong
Adam Megacz [Mon, 7 Mar 2011 13:41:46 +0000 (05:41 -0800)]
give HaskWeak its own type representation, fix numerous bugs
Adam Megacz [Mon, 7 Mar 2011 13:41:43 +0000 (05:41 -0800)]
better names for the auxiliary CaseBranch records
Adam Megacz [Mon, 7 Mar 2011 13:41:40 +0000 (05:41 -0800)]
separate type/coer/expr variables in HaskWeak case branches
Adam Megacz [Mon, 7 Mar 2011 13:41:37 +0000 (05:41 -0800)]
store variables in ELetRecBindings rather than its indexing tree
Adam Megacz [Mon, 7 Mar 2011 13:41:35 +0000 (05:41 -0800)]
add HaskWeakToCore
Adam Megacz [Mon, 7 Mar 2011 13:41:33 +0000 (05:41 -0800)]
add proper proofs of the fact that every rule has exactly one conclusion
Adam Megacz [Mon, 7 Mar 2011 13:41:30 +0000 (05:41 -0800)]
Changed WEBrak/WEEsc to store a CoreType
Adam Megacz [Mon, 7 Mar 2011 13:41:27 +0000 (05:41 -0800)]
Added WeakVar, a separate variable representation for HaskWeak
Adam Megacz [Mon, 7 Mar 2011 13:41:24 +0000 (05:41 -0800)]
added "publish" target to regenerate tex/pdf code
Adam Megacz [Mon, 7 Mar 2011 13:41:17 +0000 (05:41 -0800)]
added HaskCoreToWeak
Adam Megacz [Mon, 7 Mar 2011 13:40:58 +0000 (05:40 -0800)]
cleaned up lots of FIXMEs in ProofToLatex
Adam Megacz [Wed, 2 Mar 2011 22:25:04 +0000 (14:25 -0800)]
Initial checkin of Coq-in-GHC code