Leonardo de Moura
3e5f59d6df
chore(kernel): remove expr.quote constructor
...
In Lean4, we will reify expressions.
2018-09-07 22:08:08 -07:00
Leonardo de Moura
dd03747d22
chore(kernel): univ_param vs lparam, level_param_names ==> names, and other inconsistencies
2018-09-03 13:05:42 -07:00
Sebastian Ullrich
39cdae50ee
feat(library,frontends/lean): use mdata instead of hacky cache for position information in preterms
2018-09-02 18:08:41 -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
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
a3e5dd31b3
chore(library/locals): style
2018-06-12 17:58:25 -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
a6250840d5
chore(kernel): rename some expr functions
2018-06-09 07:18:24 -07:00
Leonardo de Moura
1612aca0b2
chore(kernel): rename expr kinds
2018-06-09 06:50:14 -07:00
Leonardo de Moura
6333043adf
refactor(kernel): abstract_local(s) ==> abstract
2018-06-07 16:28:54 -07:00
Leonardo de Moura
8dd53cd94f
chore(*): rename expr_struct_* to expr_*
...
We don't need to modifier `_struct` anymore since we don't use the
pointer equality based hashtables anymore.
2018-04-09 12:55:48 -07:00
Leonardo de Moura
faf8e025e7
chore(kernel): remove m_hash_alloc field from expressions
...
This field was originally added to create hashtables based on pointer
equality. We don't use them anymore, and the caches based on
m_hash_alloc can be implemented using m_hash without any performance
impact. This commit also fixes two places where `expr_set` was used
instead of `expr_struct_set`.
This commit is also important for the Lean4 plans where `expr` will
be implemented in Lean, and fields like `m_hash_alloc` would require us
to track state.
2018-04-09 10:05:56 -07:00
Leonardo de Moura
d73facb8bc
feat(library/init/meta/expr): add expr.has_local_in
2017-07-01 20:23:37 -07:00
Leonardo de Moura
32e6442d0a
feat(frontends/lean): no global universes in the frontend
2017-02-08 17:23:04 -08:00
Leonardo de Moura
e4c7af1373
feat(library/locals): add locals_subset predicate
2016-06-24 10:48:01 -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
1cbace9df6
feat(library/tactic/congruence_tactic): add congruence lemma generator
...
The generated congruence theorems ignore arguments that are subsingleton types.
2015-06-05 22:00:10 -07:00
Leonardo de Moura
d0d3f9bb41
refactor(kernel,library,frontends/lean): add helper functions, and cleanup collect_locals
2015-06-05 17:29:36 -07:00
Leonardo de Moura
d41bff8c43
feat(library): add helper function
2015-05-18 09:16:07 -07:00
Leonardo de Moura
9dc0388022
fix(library/tactic/rewrite_tactic): bug when rewriting hypotheses
2015-05-01 19:45:23 -07:00
Leonardo de Moura
3a67ddb7c5
feat(library/locals): use optional<expr> instead of bool at depends_on (for arrays)
2015-02-16 18:42:05 -08:00
Leonardo de Moura
2a00647089
refactor(library/tactic): cleanup 'revert' and 'clear' tactics
2014-11-26 17:08:14 -08:00
Leonardo de Moura
c28e9b9234
feat(library/tactic): add 'clear' tactic, closes #341
2014-11-26 13:11:36 -08:00
Leonardo de Moura
5c51be4585
refactor(frontends/lean): use expr_struct_set when collecting locals
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-14 04:12:58 +01:00
Leonardo de Moura
01cecb76db
feat(frontends/lean/builtin_cmds): add 'variable' command family
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-13 15:13:50 -07:00
