Leonardo de Moura 193d4dc9f5 feat: optimized deriving DecidableEq for enumeration types ... The proof term is liner on the number of constructors, but type checking is not linear because the reduction engine in the kernel is not efficient.		2021-09-08 16:21:32 -07:00
..
bench	Revert "Revert "feat: reintroduce libleanshared, link lean & leanpkg against it""	2021-08-20 09:42:05 -07:00
compiler	chore: fix some tests	2021-09-07 17:20:21 -07:00
elabissues
ir
lean	feat: optimized deriving DecidableEq for enumeration types	2021-09-08 16:21:32 -07:00
leanpkg	feat: add flag for controlling the execution of initialize commands when importing modules programmatically	2021-08-16 17:43:28 -07:00
playground	feat: add procedure for solving subgoals generated by mkSplitterProof	2021-08-24 20:23:13 -07:00
plugin
simpperf
.gitignore
common.sh