15 commits

Author	SHA1	Message	Date
Leonardo de Moura	2daeb195b5	chore: use new names	2020-11-10 10:15:19 -08:00
Leonardo de Moura	bb99fc400a	chore: remove old crap	2020-11-02 19:16:23 -08:00
Leonardo de Moura	9932c79127	chore: cleanup	2020-11-02 17:27:34 -08:00
Leonardo de Moura	a0ab1b9eb4	chore: remove with	2020-11-02 13:35:26 -08:00
Leonardo de Moura	6858cb5fb6	chore: cleanup	2020-10-29 10:24:16 -07:00
Leonardo de Moura	898a08a0c1	chore: avoid Has prefix in type classes ... closes #203	2020-10-27 18:29:19 -07:00
Leonardo de Moura	13c2a8ff51	chore: remove #lang lean4 header	2020-10-25 09:54:07 -07:00
Leonardo de Moura	1d338c4fc4	chore: move Core.lean to new frontend	2020-10-25 08:54:37 -07:00
Leonardo de Moura	522edc6743	chore: move to new frontend	2020-10-23 20:49:58 -07:00
Leonardo de Moura	dd4ae81774	chore: move to new frontend	2020-10-16 09:16:33 -07:00
Sebastian Ullrich	386c706f3e	feat: basic parenthesizer	2020-05-04 14:28:36 -07:00
Leonardo de Moura	a8c3322ac8	doc: expand dependent pattern matching support for array literals	2020-03-13 06:39:13 -07:00
Leonardo de Moura	67fb63c9fd	feat: use mpz_pow_ui to implement Nat.pow	2020-01-21 09:16:38 -08:00
Leonardo de Moura	2809cea147	chore: remove DecidableEq workaround ... We have better indexing now.	2019-11-26 17:30:18 -08:00
Leonardo de Moura	c445199747	chore: library/Init ==> src/Init ... cc @Kha @dselsam @cipher1024	2019-11-22 06:06:05 -08:00

Renamed from library/Init/Data/Nat/Basic.lean (Browse further)