leanprover / LNSym

Armv8 Native Code Symbolic Simulator in Lean
Apache License 2.0
62 stars 18 forks source link

feat: Track whether simp_mem made progress in the monad state [5/?] #234

Closed bollu closed 1 week ago

bollu commented 3 weeks ago

Description:

This approach has the advantage of making the code far less noisy. This prepares it for the refactor where we will pass goal MVarIds around, which will increase the amount of noise again 😄

Stacked on top of #233

Testing:

Non functional change, passes conformance.

License:

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.