diff options
| author | Hugo Herbelin | 2015-11-07 22:21:10 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-11-07 22:26:03 +0100 |
| commit | 479d4cd6e9934a47debf6201fccf7ebb1aea1b09 (patch) | |
| tree | a2bc3eb59a3ff6c409a488344432f30c6b2ab772 /plugins | |
| parent | c23f0cab6ee1e9c9b63347cd2624b64591871cb1 (diff) | |
Implementing assert and cut with LetIn rather than using a beta-redex.
Hopefully, it will provide with nicer proof terms, in combination with
the commit printing the type of LetIn when the defined term is a proof.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions