diff options
| author | Ryan Lahfa | 2024-06-12 13:59:11 +0200 |
|---|---|---|
| committer | Ryan Lahfa | 2024-06-12 14:27:11 +0200 |
| commit | f3b22b5cca9bc1154f55a81c9a82dc491074067d (patch) | |
| tree | 4a3f54ee8e95dbeed37a3f3d78ec0d0ac1de7883 /tests/coq/misc | |
| parent | e60d525fe3dffa035d2a551af624747dca6e1c1e (diff) | |
backends/lean: introduce `HasIntPred` automation
`HasIntPred` enable generation of facts based on specific terms in the
context rather than their types, e.g. if the "length of a list" occurs
in the context, generate the fact 0 ≤ length of that list, which can be
further used for `scalar_tac` automation to discharge bounds goals.
The aim is to use it to simplify various height related computations,
e.g. whenever "height of a (left ; right) tree" is encountered, generate
"height left < height of a (left ; right) tree", etc.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
Diffstat (limited to 'tests/coq/misc')
0 files changed, 0 insertions, 0 deletions