search

ufmg-smite / lean-smt

Tactics for discharging Lean goals into SMT solvers.
Apache License 2.0
93 stars 19 forks source link

bug fix SmtRw tactic #71

Closed mhk119 closed 10 months ago

mhk119 commented 10 months ago

This was failing before (and is now fixed)

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