leanprover / LNSym

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

refactor: make `stepiTac` directly construct an application of the right stepi-theorem #88

Closed alexkeizer closed 2 months ago

alexkeizer commented 2 months ago

Description:

Replace the simp call in stepiTac to directly construct an application of the right stepi theorem, making it much more predictable (and hopefully, performant)

Testing:

make all ran locally

License:

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