feat: remove toNat lemmas from bitvec_rules

leanprover / LNSym

Armv8 Native Code Symbolic Simulator in Lean

Apache License 2.0

62 stars 18 forks source link

feat: remove toNat lemmas from bitvec_rules #208

Closed bollu closed 1 month ago

bollu commented 1 month ago

This prevents us from unfolding expressions that have .toNat into gigantic expressions. Furthermore, this helps bv_decide, since it can see pure bitvector statements.