-
Raphaël Cauderlier authored
Coercion cannot be defined as a function, counterexamples added to test.sigma. We have to distinguish objects (ς-terms) and expressions (ς-terms with explicit coercions). In order to get an expression from an object, subtyping should be reflexive, which is only the case for well-formed types (associations lists without duplicates) so we add an invariant on types using a Σ-type. Because of these, reduction in Coq is very slow and Coq cannot check the examples yet.
c66c9c25