Leonardo de Moura
|
43ceb6bfbe
|
refactor(kernel/local_ctx): simplify local_ctx
Remark: we still need to revise the classes: `type_context` and `local_context`.
|
2018-10-24 10:02:38 -07:00 |
|
Leonardo de Moura
|
d814ee612a
|
chore(kernel/local_ctx): typo
|
2018-09-11 18:10:10 -07:00 |
|
Leonardo de Moura
|
03a99986bb
|
feat(kernel): implement local_decl using runtime
|
2018-09-08 16:25:43 -07:00 |
|
Leonardo de Moura
|
e9f843ddf6
|
refactor(kernel/expr): remove mlocal_* functions
The constructors `mvar` and `fvar` have different memory layouts.
|
2018-06-22 14:25:31 -07:00 |
|
Leonardo de Moura
|
fd5bfc7dfe
|
refactor(kernel): simplify binder_info
Now, it is an enumeration type like its Lean counterpart.
|
2018-06-20 15:31:40 -07:00 |
|
Leonardo de Moura
|
d5c24806e7
|
feat(kernel/local_ctx): add methods for replacing legacy Pi/Fun
|
2018-06-09 07:45:16 -07:00 |
|
Leonardo de Moura
|
0a5e7ff1a9
|
feat(kernel): add local_ctx
We will have only one kind of local constant (aka free variable) in
Lean4. Thus, we need a local context object to implement the kernel
type checker.
|
2018-06-06 15:24:10 -07:00 |
|