Work on type checking and decidability.
authorJoey Capper <jjc@cs.nott.ac.uk>
Fri, 27 May 2011 17:05:26 +0000 (18:05 +0100)
committerJoey Capper <jjc@cs.nott.ac.uk>
Fri, 27 May 2011 17:05:26 +0000 (18:05 +0100)
commitc807c93cf35583a9f7293aab49a403ee210df875
treebd909e7cfcf7387942f2cb9429124360240bd100
parentf8e4979912c8a76aa7a60e90adb5dbf7812931ae
Work on type checking and decidability.

Cleanup of various files. Variables renamed to \ni symbol. Convertibility split into separate file.
14 files changed:
Contexts.agda
Convertibility.agda [new file with mode: 0644]
Extraction.agda
FHM.agda
FlatEquations.agda
Infer.agda
Labeling.agda
Normalisation.agda
Normals.agda
Simplify.agda
Terms.agda
TypeTheory/Product.agda
Types.agda
Weakening.agda