• Robbert Krebbers's avatar
    Make f_equiv slightly more robust. · 5d66333c
    Robbert Krebbers authored
    Now, for example, when having equiv (Some x) (Some y) it will
    try to find a Proper whose range is an equiv before hitting the
    eq instance. My hack is general enough that it works for Forall2,
    dist, and so on, too.
    5d66333c
Name
Last commit
Last update
algebra Loading commit data...
benchmark Loading commit data...
docs Loading commit data...
heap_lang Loading commit data...
prelude Loading commit data...
program_logic Loading commit data...
proofmode Loading commit data...
tests Loading commit data...
.gitignore Loading commit data...
.gitlab-ci.yml Loading commit data...
LICENSE Loading commit data...
Makefile Loading commit data...
ProofMode.md Loading commit data...
README.md Loading commit data...
_CoqProject Loading commit data...
naming.txt Loading commit data...