13 commits

Author	SHA1	Message	Date
Leonardo de Moura	dae3489fe2	feat: remove partials from Init/Data/Array/Basic.lean	2022-01-10 16:05:33 -08:00
Leonardo de Moura	70f2200778	chore: remove enum command ... Now, `inductive` is also efficient for big enumeration types	2021-09-06 12:01:37 -07:00
Leonardo de Moura	6f075e6ece	feat: add enum command for declaring enumeration types ... closes #654	2021-09-05 16:58:49 -07:00
Leonardo de Moura	6d8058034a	chore: basic conv mode parsers	2021-09-01 15:35:32 -07:00
Leonardo de Moura	4ec85a39a5	fix: Not should not be reducible, special support for Ne ... Unification hint for `Not`	2021-02-15 17:36:11 -08:00
Leonardo de Moura	244b72befd	feat: simpArrow	2021-01-01 17:15:15 -08:00
Leonardo de Moura	df0e4808ec	feat: define tactic parsers using syntax command	2020-11-17 13:52:36 -08:00
Leonardo de Moura	99fad9fc4d	feat: goodies for writing notation with binders	2020-11-14 07:32:44 -08:00
Leonardo de Moura	8c4ac7ccc1	refactor: rename LeanInit ==> Meta, and reduce dependencies	2020-11-13 16:00:31 -08:00
Leonardo de Moura	5c33440050	chore: update Init.lean	2020-11-12 13:23:18 -08:00
Leonardo de Moura	0f3bd8abb4	feat: add rfl and decide! tactic macros	2020-10-29 16:42:22 -07:00
Leonardo de Moura	2dd1d3ac3e	chore: move ShareCommon to Std	2020-06-25 11:45:29 -07:00
Sebastian Ullrich	6a0410f8f0	feat: make import A import A.olean instead of A/Default.olean	2020-05-19 11:29:32 -07:00

Renamed from src/Init/Default.lean (Browse further)