2011-04-11 |
Adam Megacz | uncomment some code in ProgrammingLanguage.v |
commit | commitdiff | tree | snapshot |
2011-04-10 |
Adam Megacz | remove the very last admit (missing proof) from General... |
commit | commitdiff | tree | snapshot |
2011-04-10 |
Adam Megacz | add skeleton of GArrowTikZ |
commit | commitdiff | tree | snapshot |
2011-04-10 |
Adam Megacz | separate CoqPass.hs from All.v in Makefile |
commit | commitdiff | tree | snapshot |
2011-04-10 |
Adam Megacz | fix bug in GeneralizedArrowFromReification |
commit | commitdiff | tree | snapshot |
2011-04-10 |
Adam Megacz | All.v: uncomment things |
commit | commitdiff | tree | snapshot |
2011-04-10 |
Adam Megacz | bugfix in ReificationsIsomorphicToGeneralizedArrows |
commit | commitdiff | tree | snapshot |
2011-04-10 |
Adam Megacz | add commented-out definitions for analytic proofs and... |
commit | commitdiff | tree | snapshot |
2011-04-10 |
Adam Megacz | fill in lots of missing proofs |
commit | commitdiff | tree | snapshot |
2011-04-10 |
Adam Megacz | update to new coq-categories, base ND_Relation on inert... |
commit | commitdiff | tree | snapshot |
2011-04-09 |
Adam Megacz | remove notations from Preamble that come from coq-categ... |
commit | commitdiff | tree | snapshot |
2011-04-04 |
Adam Megacz | update to account for coq-categories changes |
commit | commitdiff | tree | snapshot |
2011-04-02 |
Adam Megacz | fix Makefile bug |
commit | commitdiff | tree | snapshot |
2011-04-02 |
Adam Megacz | update submodule pointer, account for changes upstream |
commit | commitdiff | tree | snapshot |
2011-04-02 |
Adam Megacz | ExtractionMain: better pdflatex code output |
commit | commitdiff | tree | snapshot |
2011-04-02 |
Adam Megacz | re-arrange ProgrammingLanguage |
commit | commitdiff | tree | snapshot |
2011-04-02 |
Adam Megacz | add extra targets to Makefile |
commit | commitdiff | tree | snapshot |
2011-04-02 |
Adam Megacz | split HaskProofCategory into two files |
commit | commitdiff | tree | snapshot |
2011-04-01 |
Adam Megacz | remove unproven step1_lemma (it has a proof now) |
commit | commitdiff | tree | snapshot |
2011-03-29 |
Adam Megacz | formatting fixes |
commit | commitdiff | tree | snapshot |
2011-03-29 |
Adam Megacz | remove stale import from ExtractionMain |
commit | commitdiff | tree | snapshot |
2011-03-29 |
Adam Megacz | lots of cleanup |
commit | commitdiff | tree | snapshot |
2011-03-29 |
Adam Megacz | tweak comments in examples |
commit | commitdiff | tree | snapshot |
2011-03-29 |
Adam Megacz | reorganized examples directory |
commit | commitdiff | tree | snapshot |
2011-03-29 |
Adam Megacz | reorganize flattening code |
commit | commitdiff | tree | snapshot |
2011-03-29 |
Adam Megacz | HaskProofCategory: more work |
commit | commitdiff | tree | snapshot |
2011-03-29 |
Adam Megacz | swap the order of the hypotheses of RLet |
commit | commitdiff | tree | snapshot |
2011-03-29 |
Adam Megacz | NaturalDeduction: remove unnecessary scnd_leaf, add... |
commit | commitdiff | tree | snapshot |
2011-03-28 |
Adam Megacz | add pushcheck |
commit | commitdiff | tree | snapshot |
2011-03-28 |
Adam Megacz | replace UJudg with Arrange |
commit | commitdiff | tree | snapshot |
2011-03-28 |
Adam Megacz | checkpoint |
commit | commitdiff | tree | snapshot |
2011-03-28 |
Adam Megacz | checkpoint |
commit | commitdiff | tree | snapshot |
2011-03-28 |
Adam Megacz | fix typo |
commit | commitdiff | tree | snapshot |
2011-03-28 |
Adam Megacz | ProgrammingLanguage: more implementation |
commit | commitdiff | tree | snapshot |
2011-03-28 |
Adam Megacz | HaskProofCategory: implement more |
commit | commitdiff | tree | snapshot |
2011-03-28 |
Adam Megacz | remove old code from WeakFunctorCategory |
commit | commitdiff | tree | snapshot |
2011-03-28 |
Adam Megacz | ReificationsIsomorphicToGeneralizedArrows: use EqDep |
commit | commitdiff | tree | snapshot |
2011-03-28 |
Adam Megacz | NaturalDeduction: allow multi-rule implementations... |
commit | commitdiff | tree | snapshot |
2011-03-28 |
Adam Megacz | Merge branch 'master' of git.megacz.com/coq-hetmet |
commit | commitdiff | tree | snapshot |
2011-03-28 |
Adam Megacz | organize Extraction-prefix.hs a bit |
commit | commitdiff | tree | snapshot |
2011-03-28 |
Adam Megacz | fallback plan: turn all CoreSyn coercions into unsafeCoerce |
commit | commitdiff | tree | snapshot |
2011-03-27 |
Adam Megacz | change name of string-extraction placeholder |
commit | commitdiff | tree | snapshot |
2011-03-27 |
Adam Megacz | remove PreCategory |
commit | commitdiff | tree | snapshot |
2011-03-27 |
Adam Megacz | Merge branch 'master' of git.megacz.com/coq-hetmet |
commit | commitdiff | tree | snapshot |
2011-03-27 |
Adam Megacz | uncomment more of the tutorial |
commit | commitdiff | tree | snapshot |
2011-03-27 |
Adam Megacz | update submodule pointer |
commit | commitdiff | tree | snapshot |
2011-03-27 |
Adam Megacz | almost finished with main theorem |
commit | commitdiff | tree | snapshot |
2011-03-27 |
Adam Megacz | fix -dont-load-proofs option in Makefile |
commit | commitdiff | tree | snapshot |
2011-03-27 |
Adam Megacz | checkpoint |
commit | commitdiff | tree | snapshot |
2011-03-27 |
Adam Megacz | get rid of vec_{fst,snd} axioms |
commit | commitdiff | tree | snapshot |
2011-03-27 |
Adam Megacz | improve error message |
commit | commitdiff | tree | snapshot |
2011-03-27 |
Adam Megacz | update submodule pointer |
commit | commitdiff | tree | snapshot |
2011-03-27 |
Adam Megacz | remove unnecessary comments |
commit | commitdiff | tree | snapshot |
2011-03-27 |
Adam Megacz | use WeakFunctorCategory to prove GArrow/Reification... |
commit | commitdiff | tree | snapshot |
2011-03-26 |
Adam Megacz | temporarily comment out |
commit | commitdiff | tree | snapshot |
2011-03-26 |
Adam Megacz | more bugfixes |
commit | commitdiff | tree | snapshot |
2011-03-26 |
Adam Megacz | fix {Reification,GeneralizedArrow}Category |
commit | commitdiff | tree | snapshot |
2011-03-26 |
Adam Megacz | improvements to ProgrammingLanguage |
commit | commitdiff | tree | snapshot |
2011-03-26 |
Adam Megacz | ProgrammingLanguage.v: add definitions for TypesL_... |
commit | commitdiff | tree | snapshot |
2011-03-26 |
Adam Megacz | finish definitions for SequentCalculus, CutRule, Sequen... |
commit | commitdiff | tree | snapshot |
2011-03-26 |
Adam Megacz | note that REmptyGroup and RLit are flat |
commit | commitdiff | tree | snapshot |
2011-03-26 |
Adam Megacz | update submodule pointer |
commit | commitdiff | tree | snapshot |
2011-03-26 |
Adam Megacz | update submodule pointer |
commit | commitdiff | tree | snapshot |
2011-03-26 |
Adam Megacz | re-arrange NaturalDeduction |
commit | commitdiff | tree | snapshot |
2011-03-26 |
Adam Megacz | change fst_zip/snd_zip to axioms |
commit | commitdiff | tree | snapshot |
2011-03-26 |
Adam Megacz | fix proof that Judgments(L) is Cartesian |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | add Concatenable, LatexMath, and fix HaskProofToLatex |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | add ToLatex instance for TyCon/TyFun |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | update categories submodule pointer |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | split Extraction.v so most can be compiled with -dont... |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | HaskProofToLatex improvements |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | HaskProofCategory: add commented-out-code |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | use apply tactic in ReificationFromGeneralizedArrow... |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | ProgrammingLanguage: significant cleanups |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | add LetRec case to Rule_Flat |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | NaturalDeductionCategory: cleanup, add SequentCalculus... |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | add ToLatex instance parameter to HaskStrong |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | remove unnecessary instance from HaskStrongTypes |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | change import order in HaskWeakVars |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | change import order in HaskCoreToWeak |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | add n-ary form of nd_weak |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | add ndr_void_proofs_irrelevant |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | move ModalBoxTyCon, ArrowTyCon to HaskLiteralsAndTyCons |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | add kindToLatex in HaskKinds |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | add ToLatex class, move machinery to General.v |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | add machinery to create merged Coq script GArrow.v |
commit | commitdiff | tree | snapshot |
2011-03-22 |
Adam Megacz | update categories submodule pointer |
commit | commitdiff | tree | snapshot |
2011-03-22 |
Adam Megacz | proofs that Types/Judgments form an enrichment |
commit | commitdiff | tree | snapshot |
2011-03-22 |
Adam Megacz | update tutorial for new GArrow classes |
commit | commitdiff | tree | snapshot |
2011-03-21 |
Adam Megacz | add distinctT, InT to General |
commit | commitdiff | tree | snapshot |
2011-03-21 |
Adam Megacz | add HaskXXXXCategory, generalized arrows, and reifications |
commit | commitdiff | tree | snapshot |
2011-03-21 |
Adam Megacz | add coq-categories as a submodule |
commit | commitdiff | tree | snapshot |
2011-03-21 |
Adam Megacz | comment out portions of the tutorial which do not yet... |
commit | commitdiff | tree | snapshot |
2011-03-21 |
Adam Megacz | Makefile update |
commit | commitdiff | tree | snapshot |
2011-03-21 |
Adam Megacz | make StrongAlt a parameter rather than field in StrongC... |
commit | commitdiff | tree | snapshot |
2011-03-20 |
Adam Megacz | remove vec2list_injective |
commit | commitdiff | tree | snapshot |
2011-03-20 |
Adam Megacz | get rid of a bunch of admits in HaskStrongToProof |
commit | commitdiff | tree | snapshot |
2011-03-20 |
Adam Megacz | require all branches of LetRec be at the same level... |
commit | commitdiff | tree | snapshot |
2011-03-20 |
Adam Megacz | add mapOptionTree_extensional, leaves_unleaves, mapleaves |
commit | commitdiff | tree | snapshot |
2011-03-20 |
Adam Megacz | add distinct_decidable, in_decidable to General.v |
commit | commitdiff | tree | snapshot |
next |