Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/pub/software/coq-hetmet
[coq-hetmet.git] / src /
drwxr-xr-x   ..
-rw-r--r-- 314 All.v
-rw-r--r-- 1336 Banner.v
-rw-r--r-- 2914 BijectionLemma.v
-rw-r--r-- 5255 Enrichments.v
-rw-r--r-- 10907 Extraction-prefix.hs
-rw-r--r-- 632 Extraction.v
-rw-r--r-- 22508 ExtractionMain.v
-rw-r--r-- 34253 General.v
-rw-r--r-- 2375 GeneralizedArrow.v
-rw-r--r-- 4544 GeneralizedArrowCategory.v
-rw-r--r-- 43172 GeneralizedArrowFromReification.v
-rw-r--r-- 2137 HaskCore.v
-rw-r--r-- 14323 HaskCoreToWeak.v
-rw-r--r-- 4520 HaskCoreTypes.v
-rw-r--r-- 1899 HaskCoreVars.v
-rw-r--r-- 47495 HaskFlattener.v
-rw-r--r-- 3887 HaskKinds.v
-rw-r--r-- 4463 HaskLiterals.v
-rw-r--r-- 6264 HaskProgrammingLanguage.v
-rw-r--r-- 11455 HaskProof.v
-rw-r--r-- 10020 HaskProofToLatex.v
-rw-r--r-- 26300 HaskProofToStrong.v
-rw-r--r-- 15467 HaskSkolemizer.v
-rw-r--r-- 6877 HaskStrong.v
-rw-r--r-- 36947 HaskStrongToProof.v
-rw-r--r-- 13654 HaskStrongToWeak.v
-rw-r--r-- 34941 HaskStrongTypes.v
-rw-r--r-- 2470 HaskTyCons.v
-rw-r--r-- 2949 HaskWeak.v
-rw-r--r-- 8183 HaskWeakToCore.v
-rw-r--r-- 33724 HaskWeakToStrong.v
-rw-r--r-- 5242 HaskWeakTypes.v
-rw-r--r-- 2553 HaskWeakVars.v
-rw-r--r-- 38914 NaturalDeduction.v
-rw-r--r-- 9494 NaturalDeductionCategory.v
-rw-r--r-- 11348 PCF.v
-rw-r--r-- 3911 Preamble.v
-rw-r--r-- 2630 ProgrammingLanguage.v
-rw-r--r-- 3163 ProgrammingLanguageArrow.v
-rw-r--r-- 22542 ProgrammingLanguageCategory.v
-rw-r--r-- 2257 ProgrammingLanguageEnrichment.v
-rw-r--r-- 3714 ProgrammingLanguageFlattening.v
-rw-r--r-- 2087 ProgrammingLanguageGeneralizedArrow.v
-rw-r--r-- 3000 ProgrammingLanguageReification.v
-rw-r--r-- 3044 Reification.v
-rw-r--r-- 5583 ReificationCategory.v
-rw-r--r-- 1997 ReificationFromGeneralizedArrow.v
-rw-r--r-- 6499 ReificationsAndGeneralizedArrows.v
-rw-r--r-- 13222 ReificationsIsomorphicToGeneralizedArrows.v
-rw-r--r-- 5038 WeakFunctorCategory.v
m--------- - categories