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
01ea596aea
refactor(kernel/expr): implement expr using runtime/object
2018-06-21 16:05:33 -07:00
Leonardo de Moura
c5714c2fac
chore(kernel): remove expr.macro constructor
...
We are now ready to implement `expr` using `runtime/object`.
2018-06-19 17:54:43 -07:00
Leonardo de Moura
9e7e600ad7
feat(kernel): add expr.proj constructor
...
TODO: implement infer_proj and reduce_proj
2018-06-19 15:45:49 -07:00
Leonardo de Moura
0847571ea6
feat(kernel): add mdata constructor
2018-06-18 13:36:22 -07:00
Leonardo de Moura
78192972e9
chore(kernel): expr_kind::Meta ==> expr_kind::MVar
2018-06-14 15:13:45 -07:00
Leonardo de Moura
73e067d361
feat(kernel): add expression literals
2018-06-14 14:55:14 -07:00
Leonardo de Moura
335c58f8a7
feat(kernel): add expr_kind::Quote
...
This is a temporary expr constructor. We need it to be able to eliminate
expr_macro, and then define expr using runtime/object
2018-06-12 17:40:00 -07:00
Leonardo de Moura
1612aca0b2
chore(kernel): rename expr kinds
2018-06-09 06:50:14 -07:00
Leonardo de Moura
0556412f8d
refactor(*): add runtime folder
...
@kha The runtime folder includes what is needed to link a
standalone Lean program. It is still contains some unnecessary files.
We will be able to remove them after we release Lean4.
2018-05-14 14:23:56 -07:00
Leonardo de Moura
3c878ecd01
feat(kernel): add let-expressions to the kernel
...
The frontend is still using the old "let-expression macros".
We will use the new let-expressions to implement the new tactic framework.
2016-02-29 16:40:17 -08:00
Leonardo de Moura
223ef58db9
fix(kernel/equiv_manager): typo
2015-03-27 10:44:09 -07:00
Leonardo de Moura
f33ad9d6f4
feat(kernel): add equivalence manager for speeding up is_def_eq
2015-03-27 10:34:54 -07:00
