Skip to content
  • Raphaël Cauderlier's avatar
    [Coq formalisation] [HUGE] Correct coercion · c66c9c25
    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