lean4-htt

Author	SHA1	Message	Date
Leonardo de Moura	4001407f10	refactor: add `MonadError` class abbreviation	2020-12-14 09:15:26 -08:00
Leonardo de Moura	0869f38de4	chore: update `structure`, `class`, `inductive`	2020-11-27 15:09:30 -08:00
Leonardo de Moura	8898988747	fix: namespace resolution	2020-11-26 08:17:35 -08:00
Leonardo de Moura	f67c93191f	feat: use `\|>.`	2020-11-19 08:38:47 -08:00
Leonardo de Moura	396e767f3d	refactor: move `Ref` to `Prelude` and rename it to `MonadRef` `MacroM` will implement `MonadRef` because 1- It will be easier to throw errors from macros 2- We will be able to `getRef` to retrieve the syntax node at macro rules. I renamed `Ref` to `MonadRef` to make it consistent with other classes providing monadic methods (e.g. `MonadEnv`, `MonadState`, etc). cc @Kha	2020-11-13 16:00:31 -08:00
Leonardo de Moura	13c2a8ff51	chore: remove `#lang lean4` header	2020-10-25 09:54:07 -07:00
Leonardo de Moura	0ab38742db	chore: cleanup	2020-10-24 06:18:01 -07:00
Leonardo de Moura	af968c60e6	chore: cleanup	2020-10-22 07:32:23 -07:00
Leonardo de Moura	b3678954f4	chore: move to new frontend	2020-10-20 17:19:05 -07:00
Leonardo de Moura	1495f403a1	chore: use `builtin_initialize` instead of `initialize` at `src/Lean`	2020-10-19 15:17:02 -07:00
Leonardo de Moura	7a8fb1b66c	chore: remove workaround `elabAppArgsAux` has been improved in the previous commit.	2020-10-11 15:08:12 -07:00
Leonardo de Moura	cd20e2ef8d	chore: use interpolated string	2020-10-11 15:08:12 -07:00
Leonardo de Moura	a53ab799d9	chore: remove workaround	2020-10-10 16:20:44 -07:00
Leonardo de Moura	069faf0a0a	chore: move `ResolveName` to new frontend	2020-10-10 13:03:46 -07:00
Leonardo de Moura	fa6b7b6393	feat: add `MonadResolveName` type class `AttrM` can now resolve names.	2020-10-10 11:33:52 -07:00
Leonardo de Moura	eacf3ed6c7	refactor: move `ResolveName` to `Lean` directory	2020-10-10 11:07:14 -07:00

16 commits