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

316 commits

Author SHA1 Message Date
Gabriel Ebner
66be9c31db refactor(library/flycheck): use flycheck_message_stream instead of option 2016-10-13 18:49:10 -07:00
Gabriel Ebner
b05b514cc2 refactor(*): structured message objects 2016-10-13 18:49:10 -07:00
Leonardo de Moura
3fbdb71f3e feat(library/tactic/simplifier): remove simp_extensions 2016-10-06 20:50:23 -07:00
Leonardo de Moura
d59410cc41 refactor(kernel): support only proof irrelevant mode 2016-09-27 17:18:52 -07:00
Leonardo de Moura
d0d75c0923 refactor(kernel): reduce number of configurations supported in the kernel 
Now, eta and impredicativity are assumed to be always true.

Motivation: the rest of the system assumes eta.
Regarding impredicativity, we decided to support only the standard library.
 2016-09-27 17:07:01 -07:00
Leonardo de Moura
9ef3ebbd5b refactor(*): delete HoTT support 2016-09-27 16:33:39 -07:00
Leonardo de Moura
89f62edaf0 refactor(library): reduce dependecies on old code, simplify normalize module 2016-09-19 22:12:34 -07:00
Leonardo de Moura
a1d36b6c4d chore(library): remove legacy_type_context 2016-09-19 21:31:21 -07:00
Leonardo de Moura
d43764b6fb refactor(library/tactic/defeq_simplifier): move defeq_simp_lemmas to library 
This commit also renames them to "rfl_lemmas".
Reason: these lemmas will be used at type_context::is_def_eq and type_context::whnf
 2016-09-12 10:36:11 -07:00
Leonardo de Moura
a74f02546b refactor(*): remove abbreviation command 2016-09-03 17:11:29 -07:00
Leonardo de Moura
a93eada058 feat(library/type_context): improved (and simplified) cache management for type_context 2016-08-23 17:56:58 -07:00
Leonardo de Moura
803c956d18 feat(util/sexpr/option_declarations): allow options to be registered after initialization 2016-08-19 16:58:30 -07:00
Leonardo de Moura
cd77f7167e chore(frontends/lean): run_tactic ==> run_command 
add `command` as alias for `tactic unit`
 2016-08-18 12:53:21 -07:00
Leonardo de Moura
ddc3789929 feat(frontends/lean): add run_tactic command 
This commit also adds the tactic `add_decl`.
 2016-08-18 10:56:18 -07:00
Daniel Selsam
a9b01991c2 feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 
Conflicts:
	src/frontends/lean/CMakeLists.txt
	src/frontends/lean/structure_cmd.h
 2016-08-17 07:34:03 -07:00
Sebastian Ullrich
751f2d8b02 refactor(frontends/lean): delegate all attribute parsing to decl_attributes 2016-08-16 13:49:03 -07:00
Leonardo de Moura
11043bc888 chore(frontends/lean/builtin_cmds): remove dead code 2016-08-11 08:38:39 -07:00
Leonardo de Moura
8ba17af50b fix(frontends/lean/builtin_cmds): non-determinism 2016-08-11 08:01:44 -07:00
Leonardo de Moura
594c7ca4c5 chore(frontends/lean/find_cmd): remove find_decl command 2016-08-03 17:32:47 -07:00
Leonardo de Moura
186d82d58d chore(frontends/lean/builtin_cmds): remove dead code 2016-08-02 15:18:05 -07:00
Leonardo de Moura
8993d0738a feat(frontends/lean): remove #elab command 
The check command is now using the new elaborator.
 2016-08-02 15:05:24 -07:00
Leonardo de Moura
9fc222b9af chore(library/pp_options): remove option pp.metavar_args 2016-07-31 16:00:21 -07:00
Leonardo de Moura
1aeda0e74b feat(frontends/lean/elaborator): invoke tactics 2016-07-31 11:56:52 -07:00
Sebastian Ullrich
e69b508492 refactor(library/export_decl): Re-implement for new scoped_ext 
Use environment_extension to persist mapping from namespaces to export
decls, use new scoped_ext to keep track of currently active export decls.
 2016-07-29 23:44:22 -04:00
Sebastian Ullrich
c4edad0372 feat(frontends/lean, library): remove attribute and metaclass scoping 
All data is now part of either a global, permanent scope or a local,
temporary one
 2016-07-29 23:44:21 -04:00
Leonardo de Moura
931251d403 feat(frontends/lean): remove local_context from parser 2016-07-28 16:19:31 -07:00
Leonardo de Moura
de9075b19d chore(frontends/lean/builtin_cmds): support 'sorry' at #elab command 2016-07-27 17:09:36 -07:00
Leonardo de Moura
3a5f6f2e64 feat(frontends/lean/builtin_cmds): improve output produced by #elab command, use kernel type checker to check elaboration result 2016-07-27 15:29:25 -07:00
Leonardo de Moura
461b5f289c feat(frontends/lean/elaborator): new elaborator skeleton 2016-07-23 19:02:17 -07:00
Leonardo de Moura
d8e6915366 fix(frontends/lean/builtin_cmds): fail if expression contain metavars 2016-07-19 13:22:10 -04:00
Leonardo de Moura
579f643d1d refactor(library): move kabstract to tactic folder 2016-07-18 09:57:02 -04:00
Leonardo de Moura
fbefda9b1c feat(frontends/lean): add commands 'add_key_equivalence' and 'print key_equivalences' 2016-07-16 15:41:32 -04:00
Daniel Selsam
9c3b7ad979 feat(simplifier/simp_extensions): basic bookkeeping 2016-07-04 17:13:19 -07:00
Leonardo de Moura
bd69aacfa8 chore(frontends/lean): remove old '#simplify' command 
We can use the new tactic framework for testing the simplifier.
 2016-06-28 11:55:02 +01:00
Leonardo de Moura
e16dbac0db feat(frontends/lean): add declare_trace command 
It allows users to define their own tracing classes.
 2016-06-28 11:45:56 +01:00
Leonardo de Moura
77286e6abb fix(frontends/lean): replay exported decls in imported files 2016-06-25 12:13:36 -07:00
Leonardo de Moura
2b43f591c9 fix(library/type_context): remove m_cache_owner field 
This idiom creates problem if we use (even accidentally) the copy constructor.
 2016-06-23 14:03:46 -07:00
Daniel Selsam
9327d85f6c chore(library/defeq_simplifier): move to new module inside library/tactic 2016-06-22 17:18:57 -07:00
Leonardo de Moura
16c050b66c reactor(library): port fun_info_manager to new type_context (and rename module to fun_info) 2016-06-21 10:42:38 -07:00
Leonardo de Moura
f4695c4a1d chore(frontends/lean): remove #defeq_simplify command 2016-06-17 10:16:53 -07:00
Daniel Selsam
a4692671e2 fix(src/library/defeq_simplifier): incorrect assertion 2016-06-14 11:31:46 -07:00
Daniel Selsam
6435dad371 fix(src/frontends/lean/builtin_cmds): typo in error message 2016-06-14 11:29:03 -07:00
Leonardo de Moura
2279807baf chore(frontends/lean): remove #tactic command 2016-06-14 11:28:52 -07:00
Leonardo de Moura
26c10c368a refactor(library): instantiate ==> instantiate_mvars 
Motivation: avoid confusion with 'instantiate' procedure for variables
 2016-06-14 10:29:47 -07:00
Leonardo de Moura
a16e3343a0 chore(library,frontends/lean): disable modules that need to be refactored 2016-06-14 10:02:11 -07:00
Leonardo de Moura
b821a521b2 fix(frontends/lean/builtin_cmds): propagate options 2016-06-09 10:56:33 -07:00
Leonardo de Moura
586e9447d1 feat(frontends/lean/builtin_cmds): add command #tactic for testing new tactic framework 2016-06-08 16:19:41 -07:00
Leonardo de Moura
224203f215 feat(library,frontends/lean/builtin_cmds): store export cmds and replay them 
see #603
closes #723
 2016-06-03 12:51:12 -07:00
Leonardo de Moura
0726db6e19 refactor(frontends/lean/builtin_cmds): separate open/export parsing from execution 2016-06-03 10:57:06 -07:00
Sebastian Ullrich
9561b45af1 fix(frontends/lean): uniform handling of declaration compound names 
* allow compound names in `namespace` and `structure`
* adjust error messages

Conflicts:
	src/frontends/lean/builtin_tactics.cpp
 2016-06-02 18:13:50 -07:00