summaryrefslogtreecommitdiff
path: root/tests/hol4/hashmap_main
diff options
context:
space:
mode:
authorRyan Lahfa2024-05-15 15:42:18 +0200
committerRyan Lahfa2024-05-24 16:07:33 +0200
commit3ff6d93822fe5b2e233d4b12b88b38839c8533c5 (patch)
tree9ea5aa8be6ba2f0f2af035d10cc50f8f05d43047 /tests/hol4/hashmap_main
parent3c8ea6df20f92be9c341bbfb748f65d6c598fead (diff)
feat: add small pieces of max theory
`0#ty` is neutral for `max` for unsigned integers. Without the `Fact` instances, those theorems are not as automatic as they could be. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
Diffstat (limited to 'tests/hol4/hashmap_main')
0 files changed, 0 insertions, 0 deletions