2011-03-28 |
Adam Megacz | replace UJudg with Arrange |
tree | commitdiff |
2011-03-28 |
Adam Megacz | checkpoint |
tree | commitdiff |
2011-03-28 |
Adam Megacz | checkpoint |
tree | commitdiff |
2011-03-28 |
Adam Megacz | fix typo |
tree | commitdiff |
2011-03-28 |
Adam Megacz | ProgrammingLanguage: more implementation |
tree | commitdiff |
2011-03-28 |
Adam Megacz | HaskProofCategory: implement more |
tree | commitdiff |
2011-03-28 |
Adam Megacz | remove old code from WeakFunctorCategory |
tree | commitdiff |
2011-03-28 |
Adam Megacz | ReificationsIsomorphicToGeneralizedArrows: use EqDep |
tree | commitdiff |
2011-03-28 |
Adam Megacz | NaturalDeduction: allow multi-rule implementations... |
tree | commitdiff |
2011-03-28 |
Adam Megacz | Merge branch 'master' of git.megacz.com/coq-hetmet |
tree | commitdiff |
2011-03-28 |
Adam Megacz | organize Extraction-prefix.hs a bit |
tree | commitdiff |
2011-03-28 |
Adam Megacz | fallback plan: turn all CoreSyn coercions into unsafeCoerce |
tree | commitdiff |
2011-03-27 |
Adam Megacz | change name of string-extraction placeholder |
tree | commitdiff |
2011-03-27 |
Adam Megacz | remove PreCategory |
tree | commitdiff |
2011-03-27 |
Adam Megacz | update submodule pointer |
tree | commitdiff |
2011-03-27 |
Adam Megacz | almost finished with main theorem |
tree | commitdiff |
2011-03-27 |
Adam Megacz | checkpoint |
tree | commitdiff |
2011-03-27 |
Adam Megacz | get rid of vec_{fst,snd} axioms |
tree | commitdiff |
2011-03-27 |
Adam Megacz | improve error message |
tree | commitdiff |
2011-03-27 |
Adam Megacz | update submodule pointer |
tree | commitdiff |
2011-03-27 |
Adam Megacz | remove unnecessary comments |
tree | commitdiff |
2011-03-27 |
Adam Megacz | use WeakFunctorCategory to prove GArrow/Reification... |
tree | commitdiff |
2011-03-26 |
Adam Megacz | temporarily comment out |
tree | commitdiff |
2011-03-26 |
Adam Megacz | more bugfixes |
tree | commitdiff |
2011-03-26 |
Adam Megacz | fix {Reification,GeneralizedArrow}Category |
tree | commitdiff |
2011-03-26 |
Adam Megacz | improvements to ProgrammingLanguage |
tree | commitdiff |
2011-03-26 |
Adam Megacz | ProgrammingLanguage.v: add definitions for TypesL_... |
tree | commitdiff |
2011-03-26 |
Adam Megacz | finish definitions for SequentCalculus, CutRule, Sequen... |
tree | commitdiff |
2011-03-26 |
Adam Megacz | note that REmptyGroup and RLit are flat |
tree | commitdiff |
2011-03-26 |
Adam Megacz | update submodule pointer |
tree | commitdiff |
2011-03-26 |
Adam Megacz | update submodule pointer |
tree | commitdiff |
2011-03-26 |
Adam Megacz | re-arrange NaturalDeduction |
tree | commitdiff |
2011-03-26 |
Adam Megacz | change fst_zip/snd_zip to axioms |
tree | commitdiff |
2011-03-26 |
Adam Megacz | fix proof that Judgments(L) is Cartesian |
tree | commitdiff |
2011-03-25 |
Adam Megacz | add Concatenable, LatexMath, and fix HaskProofToLatex |
tree | commitdiff |
2011-03-25 |
Adam Megacz | add ToLatex instance for TyCon/TyFun |
tree | commitdiff |
2011-03-25 |
Adam Megacz | update categories submodule pointer |
tree | commitdiff |
2011-03-25 |
Adam Megacz | split Extraction.v so most can be compiled with -dont... |
tree | commitdiff |
2011-03-25 |
Adam Megacz | HaskProofToLatex improvements |
tree | commitdiff |
2011-03-25 |
Adam Megacz | HaskProofCategory: add commented-out-code |
tree | commitdiff |
2011-03-25 |
Adam Megacz | use apply tactic in ReificationFromGeneralizedArrow... |
tree | commitdiff |
2011-03-25 |
Adam Megacz | ProgrammingLanguage: significant cleanups |
tree | commitdiff |
2011-03-25 |
Adam Megacz | add LetRec case to Rule_Flat |
tree | commitdiff |
2011-03-25 |
Adam Megacz | NaturalDeductionCategory: cleanup, add SequentCalculus... |
tree | commitdiff |
2011-03-25 |
Adam Megacz | add ToLatex instance parameter to HaskStrong |
tree | commitdiff |
2011-03-25 |
Adam Megacz | remove unnecessary instance from HaskStrongTypes |
tree | commitdiff |
2011-03-25 |
Adam Megacz | change import order in HaskWeakVars |
tree | commitdiff |
2011-03-25 |
Adam Megacz | change import order in HaskCoreToWeak |
tree | commitdiff |
2011-03-25 |
Adam Megacz | add n-ary form of nd_weak |
tree | commitdiff |
2011-03-25 |
Adam Megacz | add ndr_void_proofs_irrelevant |
tree | commitdiff |
2011-03-25 |
Adam Megacz | move ModalBoxTyCon, ArrowTyCon to HaskLiteralsAndTyCons |
tree | commitdiff |
2011-03-25 |
Adam Megacz | add kindToLatex in HaskKinds |
tree | commitdiff |
2011-03-25 |
Adam Megacz | add ToLatex class, move machinery to General.v |
tree | commitdiff |
2011-03-25 |
Adam Megacz | add machinery to create merged Coq script GArrow.v |
tree | commitdiff |
2011-03-22 |
Adam Megacz | update categories submodule pointer |
tree | commitdiff |
2011-03-22 |
Adam Megacz | proofs that Types/Judgments form an enrichment |
tree | commitdiff |
2011-03-21 |
Adam Megacz | add distinctT, InT to General |
tree | commitdiff |
2011-03-21 |
Adam Megacz | add HaskXXXXCategory, generalized arrows, and reifications |
tree | commitdiff |
2011-03-21 |
Adam Megacz | add coq-categories as a submodule |
tree | commitdiff |
2011-03-21 |
Adam Megacz | make StrongAlt a parameter rather than field in StrongC... |
tree | commitdiff |
2011-03-20 |
Adam Megacz | remove vec2list_injective |
tree | commitdiff |
2011-03-20 |
Adam Megacz | get rid of a bunch of admits in HaskStrongToProof |
tree | commitdiff |
2011-03-20 |
Adam Megacz | require all branches of LetRec be at the same level... |
tree | commitdiff |
2011-03-20 |
Adam Megacz | add mapOptionTree_extensional, leaves_unleaves, mapleaves |
tree | commitdiff |
2011-03-20 |
Adam Megacz | add distinct_decidable, in_decidable to General.v |
tree | commitdiff |
2011-03-19 |
Adam Megacz | checkpoint |
tree | commitdiff |
2011-03-19 |
Adam Megacz | improve HaskProofToStrong, although its messier now |
tree | commitdiff |
2011-03-19 |
Adam Megacz | add tracing support to Extraction-prefix.hs |
tree | commitdiff |
2011-03-19 |
Adam Megacz | add mapleaves to General.v |
tree | commitdiff |
2011-03-19 |
Adam Megacz | change LetRec rule to allow only a single expression... |
tree | commitdiff |
2011-03-19 |
Adam Megacz | add ToString instance for HaskStrong |
tree | commitdiff |
2011-03-19 |
Adam Megacz | add closedNDtoNormalND to NaturalDeduction |
tree | commitdiff |
2011-03-19 |
Adam Megacz | add UniqMonad |
tree | commitdiff |
2011-03-19 |
Adam Megacz | add itmap and itree_to_tree |
tree | commitdiff |
2011-03-19 |
Adam Megacz | add treeToString method to General |
tree | commitdiff |
2011-03-19 |
Adam Megacz | move Prelude_error to General.v |
tree | commitdiff |
2011-03-16 |
Adam Megacz | check for Case that uses its binder, which we do not... |
tree | commitdiff |
2011-03-16 |
Adam Megacz | fix broken sortAlts implementation |
tree | commitdiff |
2011-03-16 |
Adam Megacz | major overhaul of WeakToStrong/StrongToWeak; it can... |
tree | commitdiff |
2011-03-16 |
Adam Megacz | better variable names in HaskWeakToCore |
tree | commitdiff |
2011-03-16 |
Adam Megacz | restrict RNote to one hypothesis, major additions to... |
tree | commitdiff |
2011-03-16 |
Adam Megacz | add EGlobal/RGlobal for CoreVars whose binder we cannot see |
tree | commitdiff |
2011-03-16 |
Adam Megacz | add crude Monad type class |
tree | commitdiff |
2011-03-15 |
Adam Megacz | final batch of fixups before enabling -fcoqpass |
tree | commitdiff |
2011-03-15 |
Adam Megacz | fix spellings in Extraction-prefix.hs, minor tweaks |
tree | commitdiff |
2011-03-15 |
Adam Megacz | formatting |
tree | commitdiff |
2011-03-15 |
Adam Megacz | change names of Kind constructors to be more informative |
tree | commitdiff |
2011-03-15 |
Adam Megacz | reshuffle definitions in an attempt to iron out inter... |
tree | commitdiff |
2011-03-14 |
Adam Megacz | add support for CSP in HaskCore+HaskWeak |
tree | commitdiff |
2011-03-14 |
Adam Megacz | remove dead code from HaskWeak |
tree | commitdiff |
2011-03-14 |
Adam Megacz | eliminate ext_tree_{left,right} keywords |
tree | commitdiff |
2011-03-14 |
Adam Megacz | more formatting fixes |
tree | commitdiff |
2011-03-14 |
Adam Megacz | formatting fixes |
tree | commitdiff |
2011-03-14 |
Adam Megacz | minor cleanups, deleted dead code, eliminated use of... |
tree | commitdiff |
2011-03-14 |
Adam Megacz | fix sortAlts so it actually does something |
tree | commitdiff |
2011-03-14 |
Adam Megacz | rename weakTypeToType'' to weakTypeToTypeOfKind |
tree | commitdiff |
2011-03-14 |
Adam Megacz | revise tyFunKind to use splitKind |
tree | commitdiff |
2011-03-14 |
Adam Megacz | add splitKind to HaskKind |
tree | commitdiff |
2011-03-14 |
Adam Megacz | fix ToString instance for Kind |
tree | commitdiff |
2011-03-14 |
Adam Megacz | minor cleanups in HaskStrongToWeak |
tree | commitdiff |
next |