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>

0 files changed, 0 insertions, 0 deletions