lean4-htt

Author	SHA1	Message	Date
Leonardo de Moura	2ba3205f94	feat: add `Prod.Lex.right'`	2022-02-28 11:19:28 -08:00
Leonardo de Moura	3fbf5acbee	fix: add missing `[reducible]` annotations `Init/WF.lean`	2022-01-12 17:12:55 -08:00
Leonardo de Moura	1a6abe1dad	feat: `WellFoundedRelation` as a class	2022-01-12 08:28:03 -08:00
Leonardo de Moura	ec49c31337	chore: make sure `PSigma.lex` signature is similar to `Prod.lex`	2022-01-11 14:37:53 -08:00
Leonardo de Moura	4c051896df	refactor: `sizeofMeasure` => `sizeOfWFRel` This commit also makes the first argument of `sizeOfWFRel` implicit.	2021-09-27 19:06:10 -07:00
Leonardo de Moura	d4509878bb	feat: add `WellFoundedRelation` for `termination_by`	2021-09-25 17:21:03 -07:00
Leonardo de Moura	bb98057098	refactor: avoid `wf` suffix	2021-09-21 12:57:08 -07:00
Leonardo de Moura	10a38aef3c	chore: remove class `WellFoundedRelation` It is dead code.	2021-09-21 12:57:08 -07:00
Leonardo de Moura	9bb5d4dc93	chore: `Nat.ltWf` => `Nat.lt_wf`	2021-09-02 07:51:41 -07:00
Leonardo de Moura	a821dcbff2	chore: enforce naming convention for theorems see issue #402 fix: `ElabTerm.lean`	2021-08-07 12:48:38 -07:00
Leonardo de Moura	f4a7ffd8c8	chore: fix codebase and tests	2021-06-29 17:14:52 -07:00
Sebastian Ullrich	a02c6fd3eb	chore: adapt stdlib & tests	2021-05-20 15:17:36 -07:00
Leonardo de Moura	08d865b475	chore: remove unnecessary `generalizing`	2021-03-27 15:03:13 -07:00
Leonardo de Moura	fba719ff02	chore: adjust `WF.lean`	2021-02-01 18:08:48 -08:00
Sebastian Ullrich	0c91b3769e	chore: replace `variables` in src/	2021-01-22 14:36:05 +01:00
Leonardo de Moura	5249fdc24d	chore: cleanup and style	2020-12-12 10:36:26 -08:00
Leonardo de Moura	0869f38de4	chore: update `structure`, `class`, `inductive`	2020-11-27 15:09:30 -08:00
Leonardo de Moura	b72a3c69b6	fix: ambiguity at `induction/cases` See `efc3a320fe`	2020-11-24 14:59:12 -08:00
Leonardo de Moura	304c80d610	feat: use `<\|`	2020-11-19 09:03:38 -08:00
Leonardo de Moura	c305c2691f	chore: use `:=`	2020-11-19 07:22:31 -08:00
Leonardo de Moura	7e51020685	chore: move `SizeOf` to its own file	2020-11-10 14:43:03 -08:00
Leonardo de Moura	bf4d48f348	chore: cleanup for presentation	2020-11-05 12:43:02 -08:00
Leonardo de Moura	a6fd611db0	chore: use `generalizing`	2020-11-02 17:01:10 -08:00
Leonardo de Moura	a0ab1b9eb4	chore: remove `with`	2020-11-02 13:35:26 -08:00
Leonardo de Moura	dfc346e76f	chore: remove obsolete attribute	2020-11-02 06:47:20 -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	97c93ec557	chore: prepare to rename	2020-10-27 18:09:03 -07:00
Leonardo de Moura	13c2a8ff51	chore: remove `#lang lean4` header	2020-10-25 09:54:07 -07:00
Leonardo de Moura	535765993a	chore: move to new frontend	2020-10-23 19:59:46 -07:00
Leonardo de Moura	50990b99d6	chore: remove unnecessary annotations	2020-05-12 15:02:03 -07:00
Leonardo de Moura	33a10130cf	chore: fix stdlib	2020-05-12 15:02:03 -07:00
Leonardo de Moura	1784b0ee67	chore: `Heq` ==> `HEq`	2019-12-04 11:20:38 -08:00
Leonardo de Moura	c445199747	chore: `library/Init` ==> `src/Init` cc @Kha @dselsam @cipher1024	2019-11-22 06:06:05 -08:00

34 commits