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

287 commits

Author SHA1 Message Date
Leonardo de Moura
f72f9dd561 fix(frontends/lean/pp): purify metavar_decl_ref's 
The tests become too fragile if we don't purify them.
 2016-07-30 20:30:03 -07:00
Leonardo de Moura
b4fefd8c0b feat(frontends/lean/elaborator): coercions to functions 2016-07-30 18:54:20 -07:00
Leonardo de Moura
8b533a54c2 feat(frontends/lean/pp): improve purify_metavars 2016-07-30 15:31:06 -07:00
Leonardo de Moura
f18c84ca59 feat(frontends/lean/pp): add option for hiding coercions 2016-07-30 12:25:18 -07:00
Leonardo de Moura
a64d1a77ea refactor(library, frontends/lean): remove old coercion management module 2016-07-29 13:51:26 -07:00
Leonardo de Moura
5b0100ef0b refactor(library/lazy_abstraction): lazy ==> delayed 2016-07-27 13:53:17 -07:00
Leonardo de Moura
df1bb458f9 fix(frontends/lean/pp): use group for lambda/pi 2016-07-26 15:44:03 -07:00
Leonardo de Moura
90d920b7c9 chore(frontends/lean,library/explicit): remove dead code 2016-07-02 01:57:43 +01:00
Leonardo de Moura
fd08a9badf refactor(library/local_context): store pp_name in local_ref's 
This commit also removes the now obsolete API get_local_pp_name from abstract_type_context
 2016-06-21 10:50:38 -07:00
Leonardo de Moura
586baa4118 feat(library,frontends/lean): support for quoted expressions in the VM, compiler and frontend 
TODO: invoke elaborator at tactic.to_expr
 2016-06-15 16:06:39 -07:00
Daniel Selsam
aff7ceadee feat(src/frontends/lean/pp): look at pp.proofs when pp-ing coercions 2016-06-14 11:51:34 -07:00
Daniel Selsam
1d6de3412d fix(src/frontends/lean/pp): pp coercions that take arguments 2016-06-14 11:51:19 -07:00
Daniel Selsam
4d77f5ab2d feat(src/frontends/lean/pp): option to print theorem statements instead of proof terms 
Conflicts:
	src/frontends/lean/pp.cpp
	src/library/pp_options.cpp
 2016-06-14 11:50:53 -07:00
Leonardo de Moura
179f23b64c fix(library/lazy_abstraction): representation 2016-06-14 11:09:43 -07:00
Leonardo de Moura
546033633b feat(frontends/lean/pp): add option for pretty printing lazy-abstractions 2016-06-14 09:24:51 -07:00
Leonardo de Moura
35022dbeca feat(frontends/lean/pp): pp should not fail if infer_type fails for locals and/or metas 2016-06-13 12:26:41 -07:00
Leonardo de Moura
fe2b75aac7 fix(frontends/lean/pp,library/pp_options): 'pp.all true' should display binder types 2016-06-10 18:29:41 -07:00
Leonardo de Moura
176afb500a fix(frontends/lean/pp): make sure we are using get_local_pp_name 2016-06-10 18:29:40 -07:00
Leonardo de Moura
91204d4456 refactor(library/tactic/tactic_state): move tactic_state_format_expr to tactic_state module 2016-06-09 11:02:46 -07:00
Leonardo de Moura
222f7429e2 feat(frontends/lean/pp): pp unit.star 2016-06-08 17:30:11 -07:00
Leonardo de Moura
790980013a feat(library/init/meta): add 'trace_expr' 2016-06-08 17:27:37 -07:00
Sebastian Ullrich
647078bd40 feat(frontends/lean/pp): add option to hide binder types 
Replace old pp.hide_binder_types option

Conflicts:
        src/frontends/lean/pp.cpp
        src/library/pp_options.cpp
        src/library/pp_options.h
 2016-06-02 12:01:57 -07:00
Leonardo de Moura
53811822d4 chore(*): style 2016-05-25 18:10:15 -07:00
Leonardo de Moura
76e2f92d9c feat(frontends/lean/pp): pretty print let-expressions 2016-05-25 14:04:28 -07:00
Leonardo de Moura
6a9e5079c9 feat(library,frontends/lean/pp): add support for new string encoding 2016-05-24 16:20:43 -07:00
Leonardo de Moura
ca891c176e feat(frontends/lean/pp): add option pp.hide_comp_irrelevant 
It is true by default
 2016-05-11 11:31:38 -07:00
Leonardo de Moura
de9df69ef6 refactor(src): move compiler folder to library 2016-05-09 13:28:00 -07:00
Leonardo de Moura
93aa264060 feat(frontends/lean/pp): pretty print neutral/unreachable terms 2016-05-07 18:30:19 -07:00
Leonardo de Moura
454ec00f17 feat(frontends/lean/pp): pretty print recursive calls 2016-05-05 18:10:55 -07:00
Leonardo de Moura
da79cd7d95 feat(frontends/lean/pp): add option pp.hide_binder_types 2016-05-02 18:16:27 -07:00
Leonardo de Moura
85e7003524 refactor(compiler): expose primitive for marking computationally irrelevant terms 2016-05-02 17:33:49 -07:00
Leonardo de Moura
da8f37d7cc feat(compiler): mark computationally irrelevant terms 2016-05-02 16:23:54 -07:00
Leonardo de Moura
54f68226f4 chore(frontends/lean): disable old tactic framework and blast 2016-04-25 16:22:15 -07:00
Leonardo de Moura
fdea718d9d chore(frontends/lean): remove all #include "library/tactic.*" from frontends/lean 2016-04-25 15:41:12 -07:00
Leonardo de Moura
487a1e7f89 refactor(kernel): remove extension_context 
We replaced it with abstract_type_context
 2016-03-19 15:15:39 -07:00
Leonardo de Moura
c679c3a8d4 dev(kernel/abstract_type_context): extend abstract_type_context API 2016-03-08 11:40:36 -08:00
Leonardo de Moura
56d7fc4c23 refactor(*): cleanup replace_visitor subclasses, and make sure let-expressions are handled 2016-02-29 16:55:19 -08: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
101cf1ec4c feat(frontends/lean): remove difference between 'have' and 'assert' 2016-02-29 11:28:20 -08:00
Leonardo de Moura
eee74ef1b4 refactor(frontends/lean/pp): use abstract_type_context instead of type_checker 2016-02-26 15:35:29 -08:00
Leonardo de Moura
7d61f640f6 refactor(*): add abstract_type_context class 2016-02-26 14:17:34 -08:00
Leonardo de Moura
c9e9fee76a refactor(*): remove name_generator and use simpler mk_fresh_name 2016-02-11 18:05:57 -08:00
Leonardo de Moura
f67181baf3 chore(*): remove support for Lua 2016-02-11 17:17:55 -08:00
Leonardo de Moura
9a4a12899a fix(frontends/lean/pp): make sure pp doesn't group [] arguments 2015-12-13 12:23:22 -08:00
Leonardo de Moura
7f1800962a feat(frontends/lean/pp): allow user to override pp.all setting 
see #922
 2015-12-11 10:40:48 -08:00
Daniel Selsam
2b1e7e7759 feat(frontends/lean/pp): all disables numerals 2015-12-10 23:31:40 -08:00
Leonardo de Moura
edd1b34143 doc(library/blast/forward/pattern): describe pattern inference heuristic 2015-11-25 11:57:30 -08:00
Leonardo de Moura
017abdfb6a feat(frontends/lean): add notation for providing patterns 2015-11-24 18:48:22 -08:00
Daniel Selsam
6b06a19294 chore(frontends/lean): remove whitespace 2015-11-08 14:05:00 -08:00
Daniel Selsam
fa58d7c71e feat(frontends/lean): basic support for partial explicit 2015-11-08 14:05:00 -08:00