Leonardo de Moura
cf3b8d4eb4
chore: cleanup
...
Make the code style more uniform.
We still have a lot of leftovers from the old frontend.
2022-01-26 09:18:17 -08:00
Leonardo de Moura
7b6732a137
refactor: ExprDefEq.lean and LevelDefEq.lean are now implementation only files
...
We use the export/extern idiom to define `isLevelDefEqAux`, and then
define the `isDefEq` user facing functions at `Meta/Basic.lean`.
2021-12-06 09:57:00 -08:00
Leonardo de Moura
953dd85c06
chore: avoid inline
2021-06-28 10:17:01 -07:00
Leonardo de Moura
be841a7cad
chore: throwError! => throwError, throwErrorAt! => throwErrorAt
...
@Kha I marked the corresponding methods as `protected`.
I currently can't stand `throw_error`, and I am optimistic about
server highlighting feature you are working on :)
2021-03-11 11:59:45 -08:00
Leonardo de Moura
164577d94e
chore: remove parser! and tparser!
...
The new macros are called "leading_parser` and `trailing_parser`.
cc @Kha
2021-03-11 09:36:58 -08:00
Leonardo de Moura
c7ae8354fd
feat: improve type mismatch error messages
...
Use heuristic to automatically annotate terms with `pp.explicit`.
2020-12-17 07:11:52 -08:00
Leonardo de Moura
b4e8862716
chore: cleanup
2020-10-26 07:54:11 -07:00
Leonardo de Moura
13c2a8ff51
chore: remove #lang lean4 header
2020-10-25 09:54:07 -07:00
Leonardo de Moura
43efdd50f7
chore: move to new frontend
2020-10-14 17:38:17 -07:00
Leonardo de Moura
b7658ef91f
chore: move to new frontend
2020-10-13 17:11:52 -07:00
Leonardo de Moura
9b788db91f
feat: compute level parameters for mutually recursive definitions
2020-09-05 07:34:26 -07:00
Leonardo de Moura
5ced8867b0
feat: anonymous instances and support for all kinds of definition at mutual
2020-09-01 17:00:00 -07:00
Leonardo de Moura
9e038e331c
feat: add forallTelescopeCompatible
2020-09-01 14:46:32 -07:00
Leonardo de Moura
7bffa51d22
fix: missing file
2020-07-17 17:25:15 -07:00
