| 2011-05-15 |
Adam Megacz | fix bug in flattener, make extensionality axiom explicit
|
commit | commitdiff | tree |
| 2011-05-14 |
Adam Megacz | update examples
|
commit | commitdiff | tree |
| 2011-05-14 |
Adam Megacz | integrate skolemization pass with flattening
|
commit | commitdiff | tree |
| 2011-05-14 |
Adam Megacz | improve detection of type function kinds, mainly their...
|
commit | commitdiff | tree |
| 2011-05-14 |
Adam Megacz | add split_list to General.v
|
commit | commitdiff | tree |
| 2011-05-14 |
Adam Megacz | add ToString instance for lists
|
commit | commitdiff | tree |
| 2011-05-13 |
Adam Megacz | first draft of skolemization pass
|
commit | commitdiff | tree |
| 2011-05-13 |
Adam Megacz | add EqDecidable instances for option and Tree
|
commit | commitdiff | tree |
| 2011-05-12 |
Adam Megacz | swap order of hypotheses in RApp to match RLet
|
commit | commitdiff | tree |
| 2011-05-12 |
Adam Megacz | rewrite {take,drop}_arg_types to avoid use of equality...
|
commit | commitdiff | tree |
| 2011-05-12 |
Adam Megacz | HaskFlattener: represent first-order abstraction using...
|
commit | commitdiff | tree |
| 2011-05-12 |
Adam Megacz | HaskFlattener: use ga_mk_raw
|
commit | commitdiff | tree |
| 2011-05-12 |
Adam Megacz | update PCF.v for new ECKind
|
commit | commitdiff | tree |
| 2011-05-12 |
Adam Megacz | HaskFlattener: simplify the flattener
|
commit | commitdiff | tree |
| 2011-05-12 |
Adam Megacz | HaskStrongTypes: add {take,drop}_arg_types
|
commit | commitdiff | tree |
| 2011-05-11 |
Adam Megacz | HaskFLattener: formatting fixes and refactoring
|
commit | commitdiff | tree |
| 2011-05-10 |
Adam Megacz | start using type-family-based GArrow classes
|
commit | commitdiff | tree |
| 2011-05-10 |
Adam Megacz | have Makefile check for coq 8.3pl2-tracer
|
commit | commitdiff | tree |
| 2011-05-10 |
Adam Megacz | add examples/.build to gitignore
|
commit | commitdiff | tree |
| 2011-05-10 |
Adam Megacz | add support for flattening non-recursive Let bindings
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | move general-purpose routines from HaskFlattener to...
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | split HaskLiteralsAndTyCons into two files
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | add support for hetmet_unflatten
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | add Demo.hs
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | make GArrowTikZ into a module rather than a standalone...
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | add support for hetmet_flatten casting variable
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | allow -fcoqpass to change the type of top-level bindings
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | use the "debug" version of Outputable for ToString...
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | change ECKind to *=>*=>*
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | abstract out the kind of environment classifiers (ECKind)
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | major improvements to flattener; almost finished now
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | allow rank-1 polymorphic types for globals
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | add PairTyCon and UnitTyCon
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | minor cleanups to Extraction-prefix.hs to eliminate...
|
commit | commitdiff | tree |
| 2011-05-05 |
Adam Megacz | further improvements to flattener
|
commit | commitdiff | tree |
| 2011-05-03 |
Adam Megacz | separate HaskProofStratified into PCF.v, HaskProgrammingLang...
|
commit | commitdiff | tree |
| 2011-04-30 |
Adam Megacz | reorganize HaskProof files
|
commit | commitdiff | tree |
| 2011-04-30 |
Adam Megacz | clean up hints for NaturalDeduction, split ProgrammingLangua...
|
commit | commitdiff | tree |
| 2011-04-29 |
Adam Megacz | remove many [[admit]]s from HaskProofFlattener.v
|
commit | commitdiff | tree |
| 2011-04-27 |
Adam Megacz | Merge branch 'master' of http://git.megacz.com/coq...
|
commit | commitdiff | tree |
| 2011-04-27 |
Adam Megacz | prove all [admit]ted lemmas in HaskStrongToProof (not...
|
commit | commitdiff | tree |
| 2011-04-26 |
Adam Megacz | add Makefile target for tikz demo
|
commit | commitdiff | tree |
| 2011-04-26 |
Adam Megacz | add examples/Makefile
|
commit | commitdiff | tree |
| 2011-04-25 |
Adam Megacz | update GArrowTikZ.hs; still not finished, though
|
commit | commitdiff | tree |
| 2011-04-25 |
Adam Megacz | remove ClosedSIND (use "SIND []" instead)
|
commit | commitdiff | tree |
| 2011-04-24 |
Adam Megacz | remove all admits from ProgrammingLanguage.v
|
commit | commitdiff | tree |
| 2011-04-24 |
Adam Megacz | NaturalDeduction: add nd_swap, nd_prod_split, and some...
|
commit | commitdiff | tree |
| 2011-04-24 |
Adam Megacz | add examples targets to Makefile
|
commit | commitdiff | tree |
| 2011-04-24 |
Adam Megacz | add Unify.hs to examples
|
commit | commitdiff | tree |
| 2011-04-18 |
Adam Megacz | speed up builds by removing some dependencies from...
|
commit | commitdiff | tree |
| 2011-04-16 |
Adam Megacz | fix erroneous conclusion to penultimate lemma
|
commit | commitdiff | tree |
| 2011-04-11 |
Adam Megacz | use the $(MAKE) variable so -j2 works
|
commit | commitdiff | tree |
| 2011-04-11 |
Adam Megacz | Merge branches 'master' and 'master' of http://git...
|
commit | commitdiff | tree |
| 2011-04-11 |
Adam Megacz | unbreak lots more stuff
|
commit | commitdiff | tree |
| 2011-04-11 |
Adam Megacz | uncomment some code in ProgrammingLanguage.v
|
commit | commitdiff | tree |
| 2011-04-10 |
Adam Megacz | remove the very last admit (missing proof) from GeneralizedA...
|
commit | commitdiff | tree |
| 2011-04-10 |
Adam Megacz | add skeleton of GArrowTikZ
|
commit | commitdiff | tree |
| 2011-04-10 |
Adam Megacz | All.v: uncomment things
|
commit | commitdiff | tree |
| 2011-04-10 |
Adam Megacz | bugfix in ReificationsIsomorphicToGeneralizedArrows
|
commit | commitdiff | tree |
| 2011-04-10 |
Adam Megacz | add commented-out definitions for analytic proofs and...
|
commit | commitdiff | tree |
| 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 |
| next |
projects / coq-hetmet.git / search