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

8388 commits

Author SHA1 Message Date
Leonardo de Moura
8530e39375 fix(library/tactic/smt/congruence_closure): fixes #1430 
@dselsam I did not include your repro in the test suite because it will not work after we
enforce the `is_inner_ginductive_ir` check.
 2017-03-07 17:13:29 -08:00
Leonardo de Moura
8d3c7e7180 fix(frontends/lean/builtin_exprs): fixes #1433 2017-03-07 16:21:12 -08:00
Leonardo de Moura
839645c489 feat(library/system/io): replace io.monad with io.bind, io.return and io.map 2017-03-07 16:10:47 -08:00
Leonardo de Moura
b69e2006f5 chore(kernel/quotient/quotient): update comments 
The comments were written before the Type => Sort change
 2017-03-07 14:11:51 -08:00
Leonardo de Moura
51958df84b chore(frontends/lean/token_table): remove dead keywords 2017-03-07 14:00:49 -08:00
Leonardo de Moura
c427350dc0 chore(frontends/lean/token_table): remove dead commands 2017-03-07 13:50:14 -08:00
Daniel Selsam
7dcc36277a feat(frontends/lean/inductive_cmds.cpp): better resultant universe inference 2017-03-07 12:55:01 -08:00
Leonardo de Moura
943576b8e9 feat(library/compiler/extract_values): restrict extra_values to nat/int/char/string/name 2017-03-07 11:14:32 -08:00
Leonardo de Moura
faeac14ed7 feat(library/parray): add trace option for tracking destructive updates 2017-03-07 10:57:40 -08:00
Leonardo de Moura
f2faea9b9f refactor(frontends/lean/equations_validator): move validation code to another file 2017-03-06 14:36:42 -08:00
Daniel Selsam
4330e733c5 feat(inductive_compiler): API for is_ginductive_inner_* 2017-03-06 14:01:59 -08:00
Daniel Selsam
5f0ebf90de fix(frontends/lean/structure_cmd): call inductive compiler without params in type 2017-03-06 14:01:46 -08:00
Daniel Selsam
d122f4417a chore(src/library/print): update to use Sort 2017-03-06 14:01:33 -08:00
Leonardo de Moura
1d71103f29 feat(library/tactic/cases_tactic): add support for generalized inductive datatypes at 'cases' tactic 2017-03-06 11:49:04 -08:00
Sebastian Ullrich
2394f1faa5 fix(frontends/lean/util): do not fall back to current position 2017-03-06 11:02:51 -08:00
Sebastian Ullrich
c4ebfab14c fix(frontends/lean/structure_cmd): inheriting defaulted field depending on field starting with implicit parameter 2017-03-06 11:02:51 -08:00
Sebastian Ullrich
87b98d5aa2 fix(frontends/lean/structure_cmd): fix assertion violation when field depends on defaulted field 2017-03-06 11:02:50 -08:00
Daniel Selsam
ce1ec69ea6 fix(frontends/lean/decl_utils.cpp): closes #1417 2017-03-06 10:54:22 -08:00
Daniel Selsam
d461cb001e feat(inductive_compiler): get_ginductive_num_indices 2017-03-06 10:53:58 -08:00
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
61c9a7d466 feat(frontends/lean/elaborator): address issue described at https://github.com/leanprover/lean/issues/1403#issuecomment-282846138 
see #1403
 2017-03-05 21:01:12 -08:00
Leonardo de Moura
fa99861788 feat(frontends/lean/elaborator): add new ^. notation 
see #1403
 2017-03-05 20:12:49 -08:00
Leonardo de Moura
931820c06d chore(library/equations_compiler/structural_rec): update comment 2017-03-05 11:03:36 -08:00
Leonardo de Moura
959fa737eb fix(library/equations_compiler/structural_rec): motive for brec_on 2017-03-05 09:50:38 -08:00
Sebastian Ullrich
876a2bee46 feat(frontends/lean/elaborator): flag expr quotes containing universe params 2017-03-05 08:37:16 -08:00
Sebastian Ullrich
5d68938a9c feat(frontends/lean): expr literals ```(...) 2017-03-05 08:37:16 -08:00
Leonardo de Moura
d50da0feb7 feat(library/tactic/induction_tactic): add support for ginductive in the induction tactic 2017-03-04 14:55:35 -08:00
Leonardo de Moura
c456bceafa feat(library/tactic/cases_tactic): remove m_dep_elim since we are now always using dependent eliminators 2017-03-04 14:35:42 -08:00
Leonardo de Moura
22988bb95d feat(library/compiler): avoid pack/unpack overhead produced by the inductive_compiler in the code generator 
TODO: make sure the user is not manually using cases_on for the
auxiliary datatype generated by the inductive_compiler to
destruct nested inductives.
 2017-03-04 13:54:44 -08:00
Leonardo de Moura
060d6b66b2 fix(library/inductive_compiler/ginductive): incorrect assertion 2017-03-04 13:31:34 -08:00
Leonardo de Moura
b74740648e fix(library/tactic): fixes #1414 2017-03-03 20:50:00 -08:00
Daniel Selsam
4e1967c242 feat(inductive_compiler): is_pack and is_unpack API 2017-03-03 20:39:47 -08:00
Daniel Selsam
dc5b57bff6 fix(inductive_compiler/ginductive.cpp): populate new fields of entry 2017-03-03 20:39:39 -08:00
Daniel Selsam
616a4ce5c5 fix(inductive_compiler/ginductive.cpp): debug code did not compile 2017-03-03 20:39:27 -08:00
Daniel Selsam
e9c05f727c feat(inductive_compiler): APIs for simulated constructor offsets 2017-03-03 12:43:48 -08:00
Leonardo de Moura
d9da6f05b5 fix(library/tactic/cases_tactic): issue reported by @johoelzl at slack 2017-03-02 18:00:55 -08:00
Daniel Selsam
5ef892bb45 feat(inductive_compiler): cases_on for mutual and nested 2017-03-02 16:08:00 -08:00
Daniel Selsam
9590f2b7d0 feat(inductive_compiler): support nested inductive propositions 2017-03-02 16:01:45 -08:00
Leonardo de Moura
259d9271ab fix(library/equations_compiler): use ginductive API 
fixes #1334
 2017-03-02 15:48:03 -08:00
Leonardo de Moura
6b3e651de7 fix(library/util): get_datatype_level should not assume inductive datatype result type is a sort 
It may be something that is reducible to a sort.
 2017-03-02 11:42:16 -08:00
Leonardo de Moura
b1848efbc4 chore(library/init/meta): add head prefix to head reduction tactics, and add zeta tactic (that applies zeta reduction to all subterms) 2017-03-02 10:55:38 -08:00
Sebastian Ullrich
b9dc1c251e fix(library/inductive_compiler/ginductive_decl): assertion 2017-03-02 08:02:55 -08:00
Sebastian Ullrich
852df8872b fix(library/constructions/drec): assertion 2017-03-02 08:01:38 -08:00
Daniel Selsam
1f6306d068 perf(library/inductive_compiler): simplification with sizeof lemmas 2017-03-01 21:13:20 -08:00
Johannes Hölzl
f44cbb896c fix(src/library/equations_compiler/elim_match): handle mixing of inaccessible terms and variables 2017-03-01 21:12:42 -08:00
Leonardo de Moura
1542cd750f feat(library/tactic/induction_tactic): use drec in the induction tactic 
The new test failed before this change.
 2017-03-01 18:34:24 -08:00
Leonardo de Moura
e9f18502a7 chore(library/user_recursors): add drec_on and dcases_on 2017-03-01 15:56:06 -08:00
Leonardo de Moura
1ded3b70b8 feat(library/constructions/drec): add dcases_on 2017-03-01 15:46:19 -08:00
Leonardo de Moura
132a629eb7 fix(library/tactic/induction_tactic): use whnf when inferring C.rec name 2017-03-01 14:29:26 -08:00
Leonardo de Moura
7b0a18167b feat(library/constructions/drec): add drec_on and refactor 2017-03-01 14:12:10 -08:00