Commit 2021-05-10 14:00 622bcad3

View on Github →

feat(Tactic/PrintPrefix): better error messages

Estimated changes

Modified Mathlib/Tactic/PrintPrefix.lean

deleted structure FindOptions

added def Lean.Elab.Command.elabPrintPrefix

added structure Lean.Meta.FindOptions

added def Lean.Meta.find

added def Lean.Meta.findCore

deleted def find

deleted def findCore