Leonardo de Moura 55989c25fc chore: remove unnecessary args		2022-04-07 18:19:15 -07:00
..
InteractiveCode.lean	chore: remove unnecessary args	2022-04-07 18:19:15 -07:00
InteractiveDiagnostic.lean	chore: fix codebase after removing auto pure	2022-02-03 18:08:14 -08:00
InteractiveGoal.lean	chore: style	2022-04-07 17:35:05 -07:00
TaggedText.lean	chore: fix codebase after removing auto pure	2022-02-03 18:08:14 -08:00