max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
14060 commits 1 branch 0 tags 5.3 GiB
Commit graph

14060 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
e80765daca fix(library/export_decl): bug at export_decl_modification::perform 
The `perform` method was adding the modification to the environment
where it was being applied.
 2018-05-31 09:16:46 -07:00
Leonardo de Moura
80545832f4 chore(library): remove user attributes 2018-05-31 09:10:41 -07:00
Leonardo de Moura
f507b882e2 chore(frontends/lean): remove support for user commands from old front end 2018-05-31 09:06:07 -07:00
Leonardo de Moura
0947abaee4 chore(frontends/lean): remove broken declare_trace command 
This command is broken, and we will have a new tracing infrastructure in Lean4.
 2018-05-31 09:02:25 -07:00
Leonardo de Moura
2e8967adf1 doc(kernel/environment): document why we need is_descendant 2018-05-31 08:14:54 -07:00
Leonardo de Moura
12a03f7784 chore(frontends/lean/definition_cmds): remove dependency 2018-05-30 14:46:54 -07:00
Leonardo de Moura
4d8549305d doc(library/init/env_ext): document environment extensions in use 2018-05-30 14:28:49 -07:00
Leonardo de Moura
d3272ca1c5 refactor(frontends/lean,library/tactic/kabstract): remove add_key_equivalence command 
This command was never used in the Lean3 corelib and mathlib.
It is safe to assume it is not needed.
 2018-05-30 14:10:03 -07:00
Leonardo de Moura
d707a27c2b chore(library/class): unnecessary dependency 2018-05-30 14:05:21 -07:00
Leonardo de Moura
843cd9bacb chore(library/compiler/rec_fn_macro): remove dead code 2018-05-30 13:16:34 -07:00
Leonardo de Moura
1a369521cb chore(library/init/lean/macro): update macro TODO list 2018-05-30 10:24:31 -07:00
Leonardo de Moura
3ca2bf432f test(tests/lean/revert): add new tests for Lean without delayed abstraction macro 2018-05-30 10:19:11 -07:00
Leonardo de Moura
2ddb9d1598 refactor(library): remove delayed_abstraction macro 
We replace them with a new kind of (delayed) assignment at `metavar_context`
```
mvar := (lctx, locals, v)
```
where `lctx` is a local context, `locals` is a list of local
constants, and `v` is an expression.
When all metavariables in `v` are assigned, this assignment is replaced with
```
mvar := Fun(locals, v)
```
 2018-05-30 10:04:04 -07:00
Leonardo de Moura
c9a6f98454 chore(library/sorry): style 2018-05-29 22:27:03 -07:00
Leonardo de Moura
f7b6645b60 fix(frontends/lean/elaborator): add missing synthesize 
We added for the following reasons:
1- It should mimic the behavior of `visit_lambda` and `visit_pi`.
2- It minimizes the number of auxiliary metavariables that need to be
   created when we execute `locals.mk_lambda(new_body)`. In Lean3,
   it would minimize the number of delayed abstractions.
 2018-05-29 16:40:13 -07:00
Leonardo de Moura
7842036aba feat(library/type_context): avoid delayed_abstractions when creating binders lambda/pi/let 
This is the first step to eliminate the delayed_abstraction macro.
 2018-05-29 16:37:33 -07:00
Leonardo de Moura
73f83216c1 fix(frontends/lean/elaborator): bug at invoke_tactic 
The `is_def_eq` must be performed using the local context associated
with the metavariable.
 2018-05-29 16:34:43 -07:00
Leonardo de Moura
3615073faf fix(frontends/lean/elaborator): visit_expr_quote bug 2018-05-29 16:21:52 -07:00
Leonardo de Moura
0b1525b58e fix(library/type_context): is_quick_class bug 
It was returning false for expressions such as `let x := 10 in has_add nat`.
 2018-05-29 15:12:44 -07:00
Leonardo de Moura
978ef203b9 fix(frontends/lean/elaborator): the is_def_eq test must be performed in the right local context 2018-05-29 13:35:01 -07:00
Leonardo de Moura
14d62ab12d chore(runtime/serializer): compilation warning 2018-05-29 08:04:42 -07:00
Sebastian Ullrich
c4d7eb7949 feat(init/lean/parser/macro): global names can be overloaded 2018-05-29 16:43:32 +02:00
Leonardo de Moura
a7760631dc chore(library/init/lean/macro): document macros in use 2018-05-24 17:39:10 -07:00
Leonardo de Moura
1332fbabd6 feat(library,frontends): remove sorry macro 
Lean4 will not have macros.
 2018-05-24 14:00:30 -07:00
Leonardo de Moura
75c63ec921 refactor(*): list<name> ==> obj_list<name> 2018-05-23 15:48:43 -07:00
Leonardo de Moura
a1b9ae0e67 feat(util/obj_list): add map_reuse and cleanup code 2018-05-23 15:05:08 -07:00
Leonardo de Moura
4af1f31877 feat(util, kernel): add obj_list wrapper for Lean list objects, and use it to implement list of universe levels 2018-05-23 14:48:22 -07:00
Leonardo de Moura
ef8bbccf9f chore(util/object_ref): disable automatic coercion from object_ref to object * 2018-05-23 13:12:40 -07:00
Leonardo de Moura
e7ac7cb542 chore(cmake/Modules/cpplint.py): disable bogus cpplint check 2018-05-23 10:10:37 -07:00
Leonardo de Moura
306c300226 refactor(kernel/level): implement level on top of object 2018-05-23 09:54:46 -07:00
Leonardo de Moura
b66a088b52 fix(runtime/serializer): memory leak 2018-05-23 09:52:20 -07:00
Leonardo de Moura
3d46684d2a chore(util/name): minor change 2018-05-23 09:41:44 -07:00
Leonardo de Moura
e2a7d78dd6 chore(util/name): remove dead code 2018-05-22 17:57:33 -07:00
Leonardo de Moura
480d999e63 fix(runtime/object): bugs at string_append and string_push 2018-05-22 17:51:51 -07:00
Leonardo de Moura
7afa418e13 chore(runtime/serializer): style 2018-05-22 17:43:23 -07:00
Leonardo de Moura
339764bf6a refactor(runtime): add string_object 
The idea is to avoid the hack for storing the string unicode length.
It also reduces the amount of space used to serialize strings.
 2018-05-22 17:28:04 -07:00
Leonardo de Moura
fb00f9a780 fix(runtime/object): missing free 2018-05-22 16:50:07 -07:00
Leonardo de Moura
b2f3d3f456 chore(*): remove redundant code 2018-05-22 16:46:04 -07:00
Leonardo de Moura
5b17a30203 feat(runtime): add object serializer 
Any type implemented on top of `object` gets the serializer/deserializer for free
 2018-05-22 16:34:41 -07:00
Leonardo de Moura
67b59a0a3c fix(util): memory leaks 2018-05-22 11:05:51 -07:00
Leonardo de Moura
9a4b3f85f3 feat(library/init/lean/level): missing functions 2018-05-22 10:49:24 -07:00
Leonardo de Moura
914e702356 chore(kernel/level): remove unnecessary friend annotation 2018-05-22 09:46:17 -07:00
Leonardo de Moura
eb54a4f551 chore(kernel/cache_stack): compilation warning 2018-05-22 09:46:00 -07:00
Leonardo de Moura
4d7ae73d39 feat(library/init/lean): add level 2018-05-22 09:45:18 -07:00
Leonardo de Moura
84c0580e05 fix(library/init/meta/tactic): monad_from_pure_bind is used to implement io 2018-05-21 15:45:56 -07:00
Leonardo de Moura
160b7e8847 refactor(library/init/meta/expr): local_const will have only one field 
In Lean3, we supported two kinds of local constant:
context-less (inherited from Lean2) and context-based (type,
binder-info and pretty printing name are stored in the context).
The context-less was used in the kernel and a few modules we kept when
we moved from Lean2 to Lean3. Even if we keep the hybrind
representation, we should not expose the context-less to users.
 2018-05-21 15:36:09 -07:00
Leonardo de Moura
d04f0b2022 chore(library/init/meta): remove old code 2018-05-21 15:30:12 -07:00
Leonardo de Moura
3df91f1567 chore(*): fix tests 2018-05-21 06:57:43 -07:00
Leonardo de Moura
afd018d7cc chore(*): remove several tactics 2018-05-21 06:53:01 -07:00
Leonardo de Moura
032a101262 chore(*): remove more files 
@kha I'm trying to remove as much as possible before I start
modifying `expr`
 2018-05-21 06:42:58 -07:00