diff options
| author | Brian Campbell | 2019-10-24 14:33:57 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-10-24 14:33:57 +0100 |
| commit | 0e2b220ec96cd29471bba9f46a132427bc4b1ac4 (patch) | |
| tree | 812a5a44d3014cde683dc4128f252e2e7910209a /doc/examples/enum.sail | |
| parent | 73475b844cb09f06c78d8f8a426e9de0eeffc367 (diff) | |
Coq: use `abstract` to separate out proofs from definitions
- requires fixpoint definitions containing proofs to be processed in proof
mode (due to a bug in Coq), so change libraries and pretty printing to
do that
- adjust some lemmas to avoid extra evars
Diffstat (limited to 'doc/examples/enum.sail')
0 files changed, 0 insertions, 0 deletions