search

leanprover / LNSym

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

feat: Rewrite simp_mem to build a new expression, thereby localizing the effects of rewrites [6/?] #237

Closed bollu closed 1 week ago

bollu commented 3 weeks ago

Issues:

Resolves

Remove this section if this PR doesn't address any open issues.

Description:

A detailed description of your contribution. Why is this change necessary?

Testing:

What tests have been run? Did make all succeed for your changes? Was conformance testing successful on an Aarch64 machine?

License:

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

shigoel commented 1 week ago

@bollu Could you turn off all the tracing options so that the build is less noisy?