| 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 |
| 2011-03-19 |
Adam Megacz | add itmap and itree_to_tree
|
commit | commitdiff | tree |
| 2011-03-19 |
Adam Megacz | add treeToString method to General
|
commit | commitdiff | tree |
| 2011-03-19 |
Adam Megacz | move Prelude_error to General.v
|
commit | commitdiff | tree |
| 2011-03-16 |
Adam Megacz | expand tutorial.hs, include justification for scoping...
|
commit | commitdiff | tree |
| 2011-03-16 |
Adam Megacz | check for Case that uses its binder, which we do not...
|
commit | commitdiff | tree |
| 2011-03-16 |
Adam Megacz | Makefile fixes: ignore emacs droppings
|
commit | commitdiff | tree |
| 2011-03-16 |
Adam Megacz | fix broken sortAlts implementation
|
commit | commitdiff | tree |
| 2011-03-16 |
Adam Megacz | major overhaul of WeakToStrong/StrongToWeak; it can...
|
commit | commitdiff | tree |
| 2011-03-16 |
Adam Megacz | better variable names in HaskWeakToCore
|
commit | commitdiff | tree |
| 2011-03-16 |
Adam Megacz | restrict RNote to one hypothesis, major additions to...
|
commit | commitdiff | tree |
| 2011-03-16 |
Adam Megacz | add EGlobal/RGlobal for CoreVars whose binder we cannot see
|
commit | commitdiff | tree |
| 2011-03-16 |
Adam Megacz | add crude Monad type class
|
commit | commitdiff | tree |
| 2011-03-15 |
Adam Megacz | final batch of fixups before enabling -fcoqpass
|
commit | commitdiff | tree |
| 2011-03-15 |
Adam Megacz | fix spellings in Extraction-prefix.hs, minor tweaks
|
commit | commitdiff | tree |
| 2011-03-15 |
Adam Megacz | formatting
|
commit | commitdiff | tree |
| 2011-03-15 |
Adam Megacz | change names of Kind constructors to be more informative
|
commit | commitdiff | tree |
| 2011-03-15 |
Adam Megacz | reshuffle definitions in an attempt to iron out inter...
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | add support for CSP in HaskCore+HaskWeak
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | remove dead code from HaskWeak
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | eliminate ext_tree_{left,right} keywords
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | more formatting fixes
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | formatting fixes
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | minor cleanups, deleted dead code, eliminated use of...
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | fix sortAlts so it actually does something
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | add tutorial.coqpass to gitignore
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | add tutorial to the repository
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | rename weakTypeToType'' to weakTypeToTypeOfKind
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | revise tyFunKind to use splitKind
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | add splitKind to HaskKind
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | fix ToString instance for Kind
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | minor cleanups in HaskStrongToWeak
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | include URL for trfrac.sty and mathpartir in LaTeX...
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | first pass at proper handling of coercions in HaskWeak
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | better error reporting in HaskWeakToStrong
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | better error reporting in Extraction.v
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | close numerous holes in HaskStrongToProof
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | major revision of HaskWeakToStrong, put phi/psi on...
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | fix spelling error in HaskWeakToCore
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | remove weakTypeOfWeakExpr and replaceWeakTypeVar, no...
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | store the scrutinee CoreVar in WeakExpr Case to simplify...
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | store the magic CoreVar for hetmet brak/esc in WeakExpr...
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | detect (->) TyCon and substitute FunTy in WeakToCore
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | fix bugs in LaTeX output
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | ToString instance for HaskCore
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | General.addErrorMessage, orErrorBindWithMessage
|
commit | commitdiff | tree |
| 2011-03-14 |
Adam Megacz | move eol:string to General.v
|
commit | commitdiff | tree |
| 2011-03-13 |
Adam Megacz | restore HaskWeakToStrong functionality that I broke...
|
commit | commitdiff | tree |
| 2011-03-13 |
Adam Megacz | Remove unnecessary coreVar_eq_refl axiom
|
commit | commitdiff | tree |
| 2011-03-13 |
Adam Megacz | Rename Extraction.fail to Extraction.Prelude_error
|
commit | commitdiff | tree |
| 2011-03-13 |
Adam Megacz | Eliminate the need for WeakVar decidable equality axiom
|
commit | commitdiff | tree |
| next |
projects / coq-hetmet.git / search