• Robbert Krebbers's avatar
    Misc clean up. · cce7faa3
    Robbert Krebbers authored
    - Put code and proofs of examples in a single file.
    - Rename encode/decode to avoid conflicts with encode/decode (of the countable class) in stdpp.
    - Remove useless imports.
    cce7faa3
_CoqProject 493 Bytes