Wojciech Nawrocki 72c4717055 chore: remove dead code		2022-05-12 08:38:09 -07:00
..
InteractiveCode.lean	chore: remove dead code	2022-05-12 08:38:09 -07:00
InteractiveDiagnostic.lean	refactor: move function to PrettyPrinter	2022-05-12 08:38:09 -07:00
InteractiveGoal.lean	fix: use consistent goal prefix everywhere	2022-05-09 17:49:00 +02:00
TaggedText.lean	chore: fix codebase after removing auto pure	2022-02-03 18:08:14 -08:00