Mario Carneiro 6392c5b456 chore: import reductions		2022-09-15 14:02:38 -07:00
..
Basic.lean	chore: move Bootstrap.Dynamic -> Init.Dynamic	2022-09-02 04:36:54 -07:00
InteractiveCode.lean	fix: use delabAppExplicit for tooltips	2022-08-25 18:38:21 +02:00
InteractiveDiagnostic.lean	chore: use new comment syntax	2022-09-14 08:26:17 -07:00
InteractiveGoal.lean	refactor: RpcEncodable	2022-08-10 06:31:46 -07:00
TaggedText.lean	chore: use new comment syntax	2022-09-14 08:26:17 -07:00
UserWidget.lean	chore: import reductions	2022-09-15 14:02:38 -07:00