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

132 commits

Author SHA1 Message Date
Leonardo de Moura
045fe4ad25 fix(frontends/lean/structure_cmd): allow default values for function fields 2017-03-06 07:41:42 -08:00
Leonardo de Moura
61254847fb fix(frontends/lean/structure_cmd): when error recovery is enabled, we must not assume the expression in the fixed line is a binding expression (it may be a sorry expression) 2017-02-20 14:51:59 -08:00
Leonardo de Moura
add5266df7 fix(frontends/lean, library/tactic): error position in auto quoted terms 
This commit also gets rid of the redundant "elaborator failed" error
message.
 2017-02-09 18:03:04 -08:00
Leonardo de Moura
c09f60de6e fix(frontends/lean/structure_cmd): fixes #1347 2017-01-30 14:49:14 -08:00
Gabriel Ebner
5fdc737dfc feat(library/tactic): store name of current declaration in tactic_state 2017-01-28 08:27:19 +01:00
Sebastian Ullrich
2c3f6d0e1c fix(frontends/lean/structure_cmd): default field values of Pi type 
There were two separate issues:
* An explicit Pi as the type of a field with a default value would be considered a field reference
* An implicit Pi would be instantiated by the elaborator during `visit_structure_instance`
 2017-01-26 18:53:55 +01:00
Sebastian Ullrich
5c5c998813 fix(frontends/lean/structure_cmd): fix default field values referencing universe variables 2017-01-26 18:52:20 +01:00
Leonardo de Moura
71a7a7f466 feat(frontends/lean): add default field values 2017-01-22 21:25:49 -08:00
Leonardo de Moura
9119554835 feat(frontends/lean/structure_cmd): avoid unnecessary local_ref 2016-12-15 16:22:22 -08:00
Leonardo de Moura
6978906a78 chore(frontends/lean): remove namespace documentation 
We will add module level doc strings /-! -/
 2016-11-27 11:57:03 -08:00
Leonardo de Moura
338a46c225 fix(library/documentation): do not store doc strings for namespaces and declarations in the same name_map 2016-11-26 09:41:07 -08:00
Leonardo de Moura
97dd2f34d5 feat(library,frontends/lean): add basic doc string support 2016-11-25 18:52:56 -08:00
Gabriel Ebner
a3aced1b30 feat(frontends/lean/structure_cmd): record position of structure declaration 2016-11-08 19:22:42 -08:00
Leonardo de Moura
9b84db083d fix(frontends/lean): error localization bugs 2016-10-15 13:40:57 -07:00
Leonardo de Moura
f21f1219d9 fix(frontends/lean/structure_cmd): handle is_one_placeholder 2016-10-02 08:07:19 -07:00
Leonardo de Moura
4f69fe943a fix(frontends/lean/structure_cmd): make sure structure_cmd takes the option default_priority into account 2016-10-01 13:47:19 -07:00
Leonardo de Moura
572751c56e feat(frontends/lean): force user to use meta keyword on meta inductive/structure/class 
Before this commit, we were inferring whether an
inductive/structure/class were meta or not. This was bad since the user
had no clue whether the type was trusted (non meta) or not.
Moreover, users could get confused by this behavior and assume the
kernel was allowing trusted code to rely on untrusted one.
 2016-09-29 17:56:35 -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
5957022adb feat(frontends/lean): add 'class' keyword 2016-09-24 14:32:01 -07:00
Leonardo de Moura
b2e1e920a9 chore(frontends/lean,library,linja): remove .ilean files 2016-09-20 08:43:45 -07:00
Leonardo de Moura
ac87de33e7 fix(frontends/lean/structure_cmd): universe level validation in the structure command 2016-09-18 10:00:31 -07:00
Leonardo de Moura
6c84a0a7b1 feat(frontends/lean): use new notation for declaring universes in constant and structure decls 2016-09-13 21:45:16 -07:00
Leonardo de Moura
932d14241b chore(kernel): remove support for mutually inductive datatypes from the kernel 2016-09-10 17:39:17 -07:00
Daniel Selsam
b0c5744eea feat(inductive_compiler): support for mutually inductive types 2016-09-10 14:22:27 -07:00
Leonardo de Moura
8d9e508a11 fix(frontends/lean/structure_cmd): leftover 2016-09-10 12:57:24 -07:00
Leonardo de Moura
d8caecff49 refactor(library/exception): avoid throw_generic_exception functions 2016-09-06 12:37:56 -07:00
Leonardo de Moura
81a30a69d2 refactor(library/normalize): remove unfold and unfold_full attributes 2016-09-05 08:40:58 -07:00
Leonardo de Moura
f7df7dc9a7 refactor(kernel): add reducibility_hints 2016-09-04 16:30:02 -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
423319398d fix(frontends/lean/structure_cmd): compilation warning 2016-08-17 15:42:20 -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
Leonardo de Moura
4e0a30d21e chore(frontends/lean/structure_cmd): remove unnecessary dependency 2016-08-16 14:58:13 -07:00
Leonardo de Moura
e384b5c5f9 refactor(frontends/lean): move structure_instance to separate module 2016-08-16 14:56:09 -07:00
Leonardo de Moura
f056f0f2cb refactor(library): definitional ==> constructions 2016-08-11 10:08:22 -07:00
Leonardo de Moura
53aa89f1e1 fix(frontends/lean/structure_cmd): generate code for automatically generated coercions 2016-08-08 13:58:34 -07:00
Leonardo de Moura
1041f6d9d8 feat(frontends/lean/structure_cmd): private structures 2016-08-06 00:03:06 -07:00
Leonardo de Moura
46570bd51d fix(frontends/lean/structure_cmd): bug when generating alias for S.induction_on in the structure command 2016-08-05 23:13:39 -07:00
Leonardo de Moura
aeafe0293b feat(frontends/lean/structure_cmd): use new elaborator to process the structure command 2016-08-03 16:56:41 -07:00
Leonardo de Moura
d473622352 refactor(frontends/lean/structure_cmd): remove unnecessary options 2016-08-03 15:48:58 -07:00
Leonardo de Moura
0169989411 chore(library/class): remove transitive instance support 
Conflicts:
	src/frontends/lean/structure_cmd.cpp
	src/library/class.cpp
	src/library/class.h
 2016-07-29 23:32:10 -07: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
a64d1a77ea refactor(library, frontends/lean): remove old coercion management module 2016-07-29 13:51:26 -07:00
Leonardo de Moura
7a92ce38bd refactor(frontends/lean): elaborator_exception ==> old_elaborator_exception 2016-07-26 16:24:28 -07:00
Sebastian Ullrich
c5a8fe02ac feat(frontends/lean): add parent classes to local context in struct definitions 
Fixes #1066
 2016-07-05 19:22:08 -07:00
Daniel Selsam
aabdabdb17 fix(src/frontends/lean/structure_cmd): fixes #1036 2016-06-14 17:52:31 -07:00
Daniel Selsam
4fdf608c36 fix(src/frontends/lean/structure_cmd): check if indices are provided 2016-06-14 17:52:19 -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
Leonardo de Moura
df0d39ccee feat(kernel,library/definitional,frontends/lean/structure_cmd): make sure we can define inductive datatypes and structures containing untrusted declarations 
If they contain untrusted declarations, then the associated
declarations (e.g., constructors) will be automatically tagged as untrusted.
 2016-06-02 16:19:06 -07:00
Leonardo de Moura
dd4d115cc5 fix(frontends/lean/structure_cmd): mark recursors generated by structure cmd as auxiliary 2016-05-11 14:18:29 -07:00
Leonardo de Moura
c4f25cf15b refactor(frontends/lean): rename elaborate methods 2016-03-30 15:05:24 -07:00