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