Leonardo de Moura 9a1116d918 chore: remove <or>, first subsumes it		2020-12-22 14:10:08 -08:00
..
Control	refactor: Repr	2020-12-18 11:21:30 -08:00
Data	feat: add OfNat instance for Fin	2020-12-21 16:38:53 -08:00
System	fix: missing comma	2020-12-15 20:29:28 -08:00
Classical.lean	chore: use instance (priority := <prio>)	2020-12-21 10:17:54 -08:00
Coe.lean	chore: cleanup and style	2020-12-12 10:36:26 -08:00
Control.lean	chore: merge src/Control files	2020-11-10 18:47:23 -08:00
Core.lean	chore: use deriving Inhabited	2020-12-13 10:09:20 -08:00
Data.lean	feat: add helper classes for implementing parallel for	2020-12-19 14:15:47 -08:00
Fix.lean	refactor: arbitrary without explicit arguments	2020-11-25 09:07:38 -08:00
Meta.lean	refactor: use quotations & implicit token positions from getRef to clean up a bit	2020-12-21 17:32:36 +01:00
Notation.lean	chore: remove <or>, first subsumes it	2020-12-22 14:10:08 -08:00
NotationExtra.lean	feat: add class abbrev macro	2020-12-14 10:19:00 -08:00
Prelude.lean	feat: attach getRef position to symbols from quotations	2020-12-21 16:24:39 +01:00
SizeOf.lean	chore: update structure, class, inductive	2020-11-27 15:09:30 -08:00
System.lean	chore: remove #lang lean4 header	2020-10-25 09:54:07 -07:00
Util.lean	feat: add Prelude.lean	2020-11-10 18:08:18 -08:00
WF.lean	chore: cleanup and style	2020-12-12 10:36:26 -08:00