Ignore assumption directive for simplifier
Closed this issue · 0 comments
mn200 commented
Something like
simp[IgnAsm ‘pat’, th1]
should apply the simplifier, while ignoring the assumption(s) matching pat
.
Also
simp[NoAsms,...]
should ignore all assumptions.