bug fix: Smt rw tactic for empty lists

ufmg-smite / lean-smt

Tactics for discharging Lean goals into SMT solvers.

Apache License 2.0

93 stars 19 forks source link

Closed mhk119 closed 8 months ago

mhk119 commented 10 months ago

This wasn't working before (but now is):

example : (p1 ∧ True) = p1 := by
  smt_rw and bool_and_true [[p1], []]

mhk119 commented 8 months ago

Closed. See #76 which incorporates these changes.