michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
4426 commits 3 branches 0 tags 28 MiB
Commit graph

4426 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
e68007a727 fix(frontends/lean/builtin_tactics): adjust tactics precedence 2014-10-20 17:10:16 -07:00
Leonardo de Moura
9b8f60b739 feat(frontends/lean/builtin_exprs): tolerate dangling ',' in begin-end block 
This is useful when debugging proofs.
 2014-10-20 15:59:49 -07:00
Leonardo de Moura
a3aca96cb9 fix(frontends/lean/builtin_exprs): error position 2014-10-20 15:56:58 -07:00
Leonardo de Moura
fd40999909 feat(frontends/lean): uniform unsolved goals "error" position 2014-10-20 15:52:06 -07:00
Leonardo de Moura
c09bb3cc6f fix(tests/lean/notation): remove 'sorry' warning from expected outputs 2014-10-20 15:34:44 -07:00
Leonardo de Moura
854e72e665 refactor(library/data/list): minimize dependencies and avoid 'sorry' warning 2014-10-20 15:32:42 -07:00
Leonardo de Moura
7d0100a340 feat(library/tactic): add 'intros' tactic 2014-10-20 15:26:16 -07:00
Leonardo de Moura
5cba7244ce fix(library/tactic/expr_to_tactic): argument evaluation order is not part of the standard 2014-10-20 15:16:38 -07:00
Leonardo de Moura
33c4715f4c fix(frontends/lean/pp): suppress unnecessary '[annotation]' marks 2014-10-20 11:16:21 -07:00
Leonardo de Moura
f0cc17af87 fix(frontends/lean/elaborator): missing type information when ! operator (aka consume_args) is used 2014-10-20 08:31:36 -07:00
Leonardo de Moura
a1006073d4 feat(frontends/lean/notation_cmd): do not allow user to define new tokes containing '(', ')', ',' or change their precedence 2014-10-19 13:39:06 -07:00
Leonardo de Moura
469368f090 refactor(frontends/lean/scanner): move basic UTF8 procedures to separate module 2014-10-19 13:29:15 -07:00
Leonardo de Moura
4d4bc0551f feat(frontends/lean/pp): minimize number of spaces when pretty printing notation 2014-10-19 13:08:15 -07:00
Leonardo de Moura
ed1afe26bd feat(frontends/lean/pp): support scopedexpr notation in the pretty printer 2014-10-19 12:50:40 -07:00
Leonardo de Moura
f63d47fef3 feat(frontends/lean/pp): support foldl/foldr notation in the pretty printer 2014-10-19 11:16:24 -07:00
Leonardo de Moura
100b3abf1d fix(frontends/lean/pp): bug in notation matching procedure 2014-10-19 10:48:41 -07:00
Leonardo de Moura
d7cc7cbd8c refactor(frontends/lean/pp): remove 'reverse' hack 2014-10-19 09:56:18 -07:00
Leonardo de Moura
eef1cc4ac2 fix(frontends/lean/pp): implicit arguments in notation 2014-10-19 09:04:43 -07:00
Leonardo de Moura
85339c0cc1 fix(library/data/list/basic): mark :: as infixr 2014-10-19 08:58:52 -07:00
Leonardo de Moura
555d26aa61 feat(frontends/lean/pp): take notation declarations into account when pretty printing 
TODO: support foldl/foldr and binders
 2014-10-19 08:41:29 -07:00
Leonardo de Moura
8cfb3ae687 fix(library/module): bug in import_module 2014-10-18 21:03:22 -07:00
Leonardo de Moura
144150d47b fix(library/type): modify declaration order and make sure Type1, Type2 and Type3 notations have precedence over Type' during pretty printing 2014-10-18 15:15:44 -07:00
Leonardo de Moura
6a31a79265 refactor(frontends/lean/inductive_cmd): move auxiliary method to expr.h 2014-10-18 15:11:26 -07:00
Leonardo de Moura
eb79af98ba feat(frontends/lean/parse_config): add get_notation_entries auxiliary function for returning the list of notation declarations that start with a given head symbol 
This API is need to take notation declarations into account when pretty
printing expressions.
 2014-10-18 11:49:27 -07:00
Leonardo de Moura
f17e67efcb feat(frontends/lean/parse_table): add get_head_index auxiliary function for indexing notation declarations 2014-10-18 10:55:39 -07:00
Leonardo de Moura
f76c5bbde9 fix(init): initialization problem 2014-10-18 09:01:24 -07:00
Leonardo de Moura
2369388629 refactor(kernel/instantiate): cleanup beta-reduce 2014-10-17 20:19:51 -07:00
Leonardo de Moura
1ce3b83d79 fix(kernel/metavar): compilation error in some compilers 2014-10-17 17:22:25 -07:00
Leonardo de Moura
6285c3a217 perf(util/list): use memory pool for list cells 2014-10-17 17:08:39 -07:00
Leonardo de Moura
58aff5b4af perf(kernel/metavar): used thread local cache for instantiate_metavars 2014-10-17 17:08:35 -07:00
Leonardo de Moura
6d64da2981 perf(kernel/expr_eq_fn): use thread local cache, and avoid memory allocation/deallocation 2014-10-17 16:44:20 -07:00
Leonardo de Moura
7cc3dd0b4d chore(kernel/replace_fn): "name" constant 2014-10-17 14:20:35 -07:00
Leonardo de Moura
b6afbcb7f5 perf(kernel/replace_fn): use 'recursive' replace_fn for "small" terms 2014-10-17 14:15:09 -07:00
Leonardo de Moura
c21c8c582f feat(util/buffer): expose capacity method 2014-10-17 14:05:36 -07:00
Leonardo de Moura
10b880ce3b perf(kernel/metavar): improve occurs_expr and occurs performance 2014-10-17 14:05:22 -07:00
Leonardo de Moura
50e4c6f252 feat(util/rb_tree): add find_if method 2014-10-17 12:53:43 -07:00
Leonardo de Moura
d2cbd25985 refactor(kernel): replace_visitor doesn't need to be in the kernel anymore 2014-10-17 10:23:35 -07:00
Leonardo de Moura
14ebbda8cb perf(kernel/metavar): minor improvement 2014-10-16 21:43:54 -07:00
Leonardo de Moura
8974b52f7b perf(library/unifier): avoid unnecessary wasteful computation 2014-10-16 17:16:49 -07:00
Leonardo de Moura
fe484b26f3 refactor(kernel/expr): remove dead code 2014-10-16 13:45:36 -07:00
Leonardo de Moura
3b6b23c921 refactor(kernel/expr): remove silly overloads 2014-10-16 13:37:55 -07:00
Leonardo de Moura
c4f02bd16a refactor(kernel/expr): remove dead code 2014-10-16 13:09:26 -07:00
Leonardo de Moura
97a7dae12a refactor(kernel/expr): remove code duplication 2014-10-16 12:48:49 -07:00
Leonardo de Moura
28128e0330 fix(frontends/lean): EXTRA_TYPE info 2014-10-16 12:25:18 -07:00
Soonho Kong
5c1d23d944 feat(bin/linja): remove redundant flycheck item starting with "failed to add declaration" 
Close #247
 2014-10-15 17:05:27 -07:00
Leonardo de Moura
8907dd5b91 refactor(frontends/lean): minimize the use of 'set_tag' 2014-10-15 13:17:09 -07:00
Leonardo de Moura
814778abb1 refactor(kernel/expr): tag expressions at "creation" time 2014-10-15 13:12:09 -07:00
Leonardo de Moura
d960c1994e refactor(library/tactic/apply_tactic): reuse type_checker object 2014-10-15 09:28:01 -07:00
Leonardo de Moura
bbe4017790 refactor(library/tactic/apply_tactic): remove dead code 2014-10-15 09:15:11 -07:00
Leonardo de Moura
b94d121580 refactor(library): move flycheck "helper" classes to separate module 2014-10-15 09:08:04 -07:00