Structure FindOptions

Modification history

2021-05-10 14:00

Mathlib/Tactic/PrintPrefix.lean

feat(Tactic/PrintPrefix): better error messages

Deleted FindOptions View on Github →

2021-05-10 11:03

Mathlib/Tactic/PrintPrefix.lean

feat(Tactic/PrintPrefix): #print prefix command …

Added FindOptions View on Github →