diff options
| author | Ryan Lahfa | 2024-05-15 15:11:42 +0200 |
|---|---|---|
| committer | Ryan Lahfa | 2024-05-21 10:42:15 +0200 |
| commit | 065e60754084ef169fd17bbb7ab1b492fb7497c3 (patch) | |
| tree | a47a7ea9f04c31d197e2c1198bada4c4ac932369 /tests/hol4/betree/betreeMain_OpaqueScript.sml | |
| parent | cbf425d178f9063507585233ebee7ca785567e3a (diff) | |
feat(backends/lean): make `max`-related coercions nicer
Situations where you have `coe (max a b) = max (coe a) (coe b)` are
often stuck during verification because of the lack of this theorem.
With this theorem, `push_cast` works as intended and normalizes even
further.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
Diffstat (limited to 'tests/hol4/betree/betreeMain_OpaqueScript.sml')
0 files changed, 0 insertions, 0 deletions