Commit 2023-06-29 11:49 82f200da

View on Github →

fix: have tauto use Lean.Meta.isProp rather than Lean.Expr.isProp (#5565) Lean.Expr.isProp can't handle metavariables but Lean.Meta.isProp can. Bug reported by @negiizhao

Estimated changes