leanprover / LNSym

Armv8 Native Code Symbolic Simulator in Lean
Apache License 2.0
51 stars 13 forks source link

chore: remove old versions of the sym tactic, and rename the new `sym1_n` tactic to `sym_n` #94

Closed alexkeizer closed 4 weeks ago

alexkeizer commented 1 month ago

Depends on #92

Description:

Relatively minor cleanup that removes the old versions of symbolic simulation in favor of the new sym1_n tactic, which I subsequently renamed to the more intuitive sym_n, now that this name is available.

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.

alexkeizer commented 4 weeks ago

@shigoel, this should be ready to merge now