Closed bollu closed 1 week ago
This ensures that one part of the infrastructure is written completely in terms of MetaM. We will give simp_mem the same treatment next.
simp_mem
PR stacked on top of https://github.com/leanprover/LNSym/pull/232
No executable defs have changed, cosim succeeds.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.
Description:
This ensures that one part of the infrastructure is written completely in terms of MetaM. We will give
simp_memthe same treatment next.PR stacked on top of https://github.com/leanprover/LNSym/pull/232
Testing:
No executable defs have changed, cosim succeeds.
License:
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.