Leonardo de Moura
|
4fbb65d9f1
|
feat(frontends/lean,library/equations_compiler): store tactics for generating well founded relation and decreasing proofs
|
2017-05-23 15:00:29 -07:00 |
|
Gabriel Ebner
|
47629e9da3
|
feat(frontends/lean): make most parser_errors recoverable
|
2017-05-23 11:14:31 -07:00 |
|
Gabriel Ebner
|
95300224aa
|
fix(frontends/lean/builtin_cmds): suppress unhelpful #check output
|
2017-05-23 11:14:31 -07:00 |
|
Gabriel Ebner
|
183bf63e26
|
fix(frontends/lean/parser): pass error-recovery flag from parser to elaborator
|
2017-05-23 11:14:31 -07:00 |
|
Gabriel Ebner
|
77a2311f09
|
fix(frontends/lean/elaborator): segfault
|
2017-05-23 11:14:31 -07:00 |
|
Gabriel Ebner
|
166c07e1fe
|
fix(frontends/lean/elaborator): do not leak _elab_u names
|
2017-05-23 11:14:31 -07:00 |
|
Gabriel Ebner
|
d27a0eff15
|
chore(tests): fix tests
|
2017-05-23 11:14:31 -07:00 |
|
Gabriel Ebner
|
f24d790416
|
chore(tests/lean/fail): update to current syntax
|
2017-05-23 11:14:31 -07:00 |
|
Gabriel Ebner
|
99754188e6
|
feat(library/compiler/eta_expansion): also eta-expand expressions containing sorry
|
2017-05-23 11:14:31 -07:00 |
|
Gabriel Ebner
|
af63d4036b
|
chore(tests): update tests
|
2017-05-23 11:14:31 -07:00 |
|
Gabriel Ebner
|
8bd09fe282
|
chore(tests): add demo for parser error recovery
|
2017-05-23 11:14:30 -07:00 |
|
Gabriel Ebner
|
89ad117be3
|
chore(tests): update tests with changes to error recovery
|
2017-05-23 11:14:30 -07:00 |
|
Sebastian Ullrich
|
49e5c69447
|
fix(init/meta/expr): have all reflected defns accept Sort
|
2017-05-23 11:00:33 +02:00 |
|
Sebastian Ullrich
|
5a19430f60
|
fix(frontends/lean/scanner): wrong upos after field projection
|
2017-05-23 10:33:31 +02:00 |
|
Gabriel Ebner
|
5d6bf38b7e
|
chore(tests): add Leo's test case for errors in solve1-blocks
|
2017-05-23 07:33:12 +02:00 |
|
Gabriel Ebner
|
54114fd7bd
|
fix(frontends/lean/tactic_notation): do not clamp errors to the end of {} blocks
|
2017-05-23 07:28:34 +02:00 |
|
Gabriel Ebner
|
fbfec02015
|
fix(tests): move test away from run
|
2017-05-22 17:51:10 +02:00 |
|
Gabriel Ebner
|
cb28f382a3
|
fix(library/equations_compiler/elim_match): handle partially applied constructors
|
2017-05-22 17:17:27 +02:00 |
|
Leonardo de Moura
|
3d088eea25
|
fix(library/equations_compiler): avoid name collision when pack_mutual is not used
|
2017-05-21 15:40:06 -07:00 |
|
Leonardo de Moura
|
f742d9c9d8
|
feat(library/equations_compiler/pack_domain): use psigma instead of sigma
|
2017-05-20 19:14:10 -07:00 |
|
Leonardo de Moura
|
fa863496da
|
feat(library/equations_compiler): prove equational lemmas for auxiliary definition
|
2017-05-20 16:38:32 -07:00 |
|
Daniel Selsam
|
0bc855149a
|
feat(inductive_compiler): generate sizeof_spec for nested constructors
|
2017-05-20 08:30:57 -07:00 |
|
Sebastian Ullrich
|
9507297687
|
fix(init/meta/expr,library): reflect should accept Props
Fixes #1590
|
2017-05-19 14:17:06 +02:00 |
|
Leonardo de Moura
|
b69cf7ef43
|
fix(library/tactic/rewrite_tactic): instantiate assign metavars before rewriting
fixes #1587
|
2017-05-18 10:57:03 -07:00 |
|
Sebastian Ullrich
|
9b86808345
|
fix(frontends/lean/structure_cmd): parent structures may use different universe params
Fixes #1585
|
2017-05-18 09:35:14 -07:00 |
|
Sebastian Ullrich
|
9fdf11fa54
|
fix(frontends/lean/pp): shadowing shortened const
Fixes #1584
|
2017-05-18 09:35:14 -07:00 |
|
Leonardo de Moura
|
737136e8fd
|
feat(library/equations_compiler/wf_rec): apply well_founded.fix
|
2017-05-17 16:44:53 -07:00 |
|
Leonardo de Moura
|
7cf848cbb2
|
chore(tests/lean/run/wfrec1): cleanup example
|
2017-05-17 16:06:45 -07:00 |
|
Leonardo de Moura
|
56823a22b7
|
feat(library/equations_compiler/wf_rec): use has_well_founded type class to generate default well founded relation when one is not provided
|
2017-05-17 14:37:21 -07:00 |
|
Leonardo de Moura
|
dea8a856dc
|
chore(library/equations_compiler/compiler): generate error when using well founded recursion in meta definitions
|
2017-05-17 12:24:47 -07:00 |
|
Sebastian Ullrich
|
75786e9a6e
|
feat(frontends/lean/pp): hide (some) defaulted arguments on pp.implicit true
|
2017-05-17 10:38:12 -07:00 |
|
Sebastian Ullrich
|
84997bf4de
|
refactor(init/meta/expr): unify expr and pexpr
|
2017-05-17 10:38:12 -07:00 |
|
Leonardo de Moura
|
7d2ec25e81
|
fix(tests/lean/interactive/complete_field): fix tests
|
2017-05-16 14:50:15 -07:00 |
|
Leonardo de Moura
|
0091cef9f2
|
feat(library/tactic): start algebraic normalizer
|
2017-05-15 21:46:19 -07:00 |
|
Leonardo de Moura
|
4575c9e038
|
feat(frontends/lean): swap (t) and ``(t) semantics
|
2017-05-15 09:41:31 -07:00 |
|
Leonardo de Moura
|
76ff23c154
|
chore(tests/lean): fix tests
|
2017-05-14 19:40:36 -07:00 |
|
Mario Carneiro
|
7ace147f25
|
refactor(init/meta/tactic): replace assertv -> note, definev -> pose
|
2017-05-14 19:34:27 -07:00 |
|
Sebastian Ullrich
|
27c1d2f4fb
|
fix(init/meta/interactive): simp: accept local refs as simp names
|
2017-05-14 19:19:22 -07:00 |
|
Sebastian Ullrich
|
14425bd2d3
|
fix(frontends/lean/decl_util): double-elaboration of include params
|
2017-05-14 19:19:22 -07:00 |
|
Gabriel Ebner
|
85673cdd8d
|
fix(frontends/lean/definition_cmds): examples in noncomputable theories
|
2017-05-13 09:04:07 +02:00 |
|
Sebastian Ullrich
|
4b21b13649
|
refactor(init): replace has_quote class with reflected
|
2017-05-09 16:02:42 -07:00 |
|
Sebastian Ullrich
|
ead6318ee0
|
feat(frontends/lean/elaborator): substitute reflected locals into expr quotes
|
2017-05-09 16:02:41 -07:00 |
|
Sebastian Ullrich
|
2825c5fbcc
|
feat(frontends/lean/elaborator): elaborate ``(e) to type reflected e` if possible and add coercion reflected -> expr
|
2017-05-09 16:02:41 -07:00 |
|
Sebastian Ullrich
|
aa601d3e51
|
chore(tests): move tests to correct dir
|
2017-05-09 16:02:41 -07:00 |
|
Gabriel Ebner
|
b536df3596
|
feat(library/type_context): add option to unfold lemmas
|
2017-05-08 10:14:47 -07:00 |
|
Gabriel Ebner
|
40bf75cbff
|
fix(library/equations_compiler/structural_rec): fix indices
|
2017-05-07 15:52:39 +02:00 |
|
Gabriel Ebner
|
4b22e2309c
|
refactor(system/io): use spawn_args structure in all process functions
|
2017-05-04 16:41:11 -07:00 |
|
Gabriel Ebner
|
f0d22ed3e5
|
feat(library/process,system/io): set environment variables for spawned processes
|
2017-05-04 16:41:11 -07:00 |
|
Daniel Selsam
|
b7d20a333f
|
chore(src/library/constants): rm unused constants
|
2017-05-04 16:34:32 -07:00 |
|
Sebastian Ullrich
|
ad4f8cec73
|
chore(tests): forgot to commit test
|
2017-05-03 13:27:35 -07:00 |
|