• Johannes Kloos's avatar
    Proofs of infinity and Fresh instances. · 3a262d02
    Johannes Kloos authored
    We prove that various types are infinite, notably:
    - nat, N, positive and Z;
    - string (using pretty-printing of nat);
    - option, with an infinite element type;
    - list, with an inhabited element type.
    
    Furthermore, we instantiate Fresh for strings.
    3a262d02
_CoqProject 867 Bytes