lean4-htt

Author	SHA1	Message	Date
Leonardo de Moura	f4a7ffd8c8	chore: fix codebase and tests	2021-06-29 17:14:52 -07:00
Leonardo de Moura	9d12856432	feat: missing `forM`	2021-04-03 18:24:31 -07:00
Leonardo de Moura	aae8a35150	feat: add `ForIn` type class	2021-02-04 17:59:44 -08:00
Sebastian Ullrich	0c91b3769e	chore: replace `variables` in src/	2021-01-22 14:36:05 +01:00
Leonardo de Moura	04a07c15b9	chore: use `deriving Inhabited`	2020-12-13 11:57:59 -08:00
Leonardo de Moura	0869f38de4	chore: update `structure`, `class`, `inductive`	2020-11-27 15:09:30 -08:00
Leonardo de Moura	c305c2691f	chore: use `:=`	2020-11-19 07:22:31 -08:00
Leonardo de Moura	81d6e065e7	chore: adjust files and tests	2020-11-07 17:32:12 -08:00
Leonardo de Moura	63a5baafac	chore: cleanup	2020-10-28 22:03:50 -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	1ce2cde099	chore: move to new frontend	2020-10-17 14:01:25 -07:00
Leonardo de Moura	6be71b337f	refactor: add `prototype2.lean`	2020-08-04 18:35:11 -07:00
Leonardo de Moura	943446f1b3	fix: `FVarSubst` must be a mapping from `FVarId` to `Expr` Reason: `subst` tactic must store the `x \|-> e` when substituting `x` with `e`.	2020-08-04 13:06:08 -07:00
Leonardo de Moura	02aa8498cd	chore: move `AssocList` to `Std`	2020-06-25 12:52:23 -07:00