lean4-htt

Author	SHA1	Message	Date
Leonardo de Moura	d43a1c7d9a	chore: move `Constructions` to `Meta`	2021-09-06 10:51:11 -07:00
Leonardo de Moura	f4ecbd1102	chore: reduce dependencies	2021-08-24 17:38:43 -07:00
Leonardo de Moura	d52de3392b	chore: remove workaround	2021-08-13 19:35:47 -07:00
Leonardo de Moura	a15a36b8d3	chore: cleanup `Subarray` instances	2021-08-13 19:29:09 -07:00
Leonardo de Moura	4b58c4cc02	refactor: instances that "hide" coercions Example: ``` instance [CoeHTCT α β] [Add β] : HAdd α β β where hAdd a b := Add.add a b ```	2021-08-13 17:18:55 -07:00
Leonardo de Moura	be23709737	chore: use `binop%` to define `++` notation	2021-08-13 16:26:35 -07:00
Daniel Fabian	9200de01ef	refactor: fix code review comments.	2021-06-06 06:40:09 -07:00
Daniel Fabian	968ae18f20	fix: deal with params for inductive predicates.	2021-06-06 06:40:09 -07:00
Daniel Fabian	4e53b3bdbf	fix: use motive from `brecOn` in structural recursion for predicates.	2021-06-06 06:40:09 -07:00
Daniel Fabian	822c551aa2	test: Add a bunch of test for structural recursion on predicates.	2021-06-06 06:40:09 -07:00
Daniel Fabian	ec6f7d9bd6	feat: Implement structural recursion for inductive predicates.	2021-06-06 06:40:09 -07:00
Daniel Fabian	c426a816a1	refactor: Make the non-below version of a premise in the below type for inductive predicates implicit. Since it is always fully implied by the below version thereof, it carries no real information and shouldn't be used in pattern matching.	2021-05-22 18:09:32 -07:00
Daniel Fabian	ab0ef229ac	feat: add `getBelowIndices`.	2021-05-19 07:28:14 -07:00
Daniel Fabian	d54c964a51	fix: improve the tactic for brecOn for inductive predicates.	2021-04-29 17:19:09 -07:00
Daniel Fabian	1f05f5bf11	chore: rename ProofBelow to below.	2021-04-26 20:33:21 +02:00

15 commits