major improvements to flattener; almost finished now
[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-- 10220 Extraction-prefix.hs
-rw-r--r-- 632 Extraction.v
-rw-r--r-- 22368 ExtractionMain.v
-rw-r--r-- 29904 General.v
-rw-r--r-- 2375 GeneralizedArrow.v
-rw-r--r-- 4544 GeneralizedArrowCategory.v
-rw-r--r-- 43172 GeneralizedArrowFromReification.v
-rw-r--r-- 2119 HaskCore.v
-rw-r--r-- 13876 HaskCoreToWeak.v
-rw-r--r-- 4366 HaskCoreTypes.v
-rw-r--r-- 1881 HaskCoreVars.v
-rw-r--r-- 42881 HaskFlattener.v
-rw-r--r-- 3785 HaskKinds.v
-rw-r--r-- 6370 HaskLiteralsAndTyCons.v
-rw-r--r-- 6246 HaskProgrammingLanguage.v
-rw-r--r-- 10589 HaskProof.v
-rw-r--r-- 10004 HaskProofToLatex.v
-rw-r--r-- 26300 HaskProofToStrong.v
-rw-r--r-- 6859 HaskStrong.v
-rw-r--r-- 36946 HaskStrongToProof.v
-rw-r--r-- 13636 HaskStrongToWeak.v
-rw-r--r-- 30278 HaskStrongTypes.v
-rw-r--r-- 2931 HaskWeak.v
-rw-r--r-- 8165 HaskWeakToCore.v
-rw-r--r-- 33181 HaskWeakToStrong.v
-rw-r--r-- 5201 HaskWeakTypes.v
-rw-r--r-- 2559 HaskWeakVars.v
-rw-r--r-- 38914 NaturalDeduction.v
-rw-r--r-- 9494 NaturalDeductionCategory.v
-rw-r--r-- 11318 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