Leonardo de Moura
3a878bd3f4
fix(frontends/lean/interactive): compilation warning with older versions of g++
2017-03-21 08:31:16 -07:00
Leonardo de Moura
aa68d72fa5
fix(library/equations_compiler/elim_match): skip nonvar + inaccessible
2017-03-21 08:08:36 -07:00
Leonardo de Moura
fdadada3a9
fix(frontends/lean): fixes #1468
...
@kha I had to add yet another hack to fix this issue.
In notation declarations, names are resolved at notation declaration time.
So, users do not expect them to be resolved again at tactic execution time.
I addressed this problem by wrapping constants occurring in notation
declarations with a "frozen_name" annotation. This transformation is
only performed if m_in_quote is true.
Then resolve_names_fn at elaborator.cpp will not try to resolve the
names again.
This change broke two other modules. `-` notation for inverting
equations at `rw`, and `calc` expressions inside quotes.
The broke for the same reason. They were not expecting the constants
to be wrapped with an annotation.
2017-03-18 13:48:21 -07:00
Leonardo de Moura
31b6dc222d
feat(library/init/meta/expr): add expr.is_annotation
2017-03-18 13:40:11 -07:00
Leonardo de Moura
3322adde1b
fix(library/tactic/subst_tactic): fixes #1467
2017-03-17 19:54:35 -07:00
Sebastian Ullrich
5e0e19c4ad
fix(frontends/lean/{interactive,tactic_notation}): fix tests
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
60a244e4f9
fix(frontends/lean,shell): fix file dependencies
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
7c31e62b16
feat(init/meta/interactive): improve pretty-printing of list_of and itactic
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
e0856284b0
feat(frontends/lean,emacs): tactic info before elaboration, fix many edge cases
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
421a6d6f01
feat(frontends/lean/interactive,emacs): highlight current tactic parameter
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
24e7e87f7d
feat(frontends/lean/tactic_notation): fall back to tactic info when hovering over/between parameters
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
9b5e7ddcda
feat(frontends/lean/interactive,emacs): hide colon separator in front of pretty-printed types
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
c46936d180
fix(frontends/lean/interactive): hard-code tactic pretty printing
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
e3a65ee794
refactor(frontends/lean/interactive,shell/server): factor out JSON reporting code
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
803d3073ae
feat(frontends/lean): add interactive.type_formatter attribute and use it to pretty print interactive tactics
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
0792bc13db
feat(frontends/lean/elaborator,init/meta/interactive): relax expr pattern elaboration and use it to implement a tactic signature pretty printer
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
ae3e685c1f
chore(tests/lean): forgot to add test case
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
c387c34365
fix(test/lean/interactive/run_single): include stderr
2017-03-17 18:05:19 -07:00
Sebastian Ullrich
9137248707
fix(library/vm/vm_rb_map): assertion violation in destructor of vb_rb_map_ts_copy with nat keys or values
2017-03-17 18:05:11 -07:00
Gabriel Ebner
886c824e33
feat(library/init/data/list/instances): prove decidability of bounded quantification
2017-03-17 18:03:26 -07:00
Leonardo de Moura
b803377d5e
fix(library/tactic/smt/congruence_closure): relation used to implement congruence tables was not transitive
2017-03-17 16:04:41 -07:00
Leonardo de Moura
ed9e6fb940
chore(tests/lean/type_error_at_eval_expr): fix test
2017-03-17 14:46:41 -07:00
Leonardo de Moura
8ff176717c
feat(library/tactic/smt/congruence_closure): add check_congr_keys assertions
2017-03-17 13:48:12 -07:00
Leonardo de Moura
37c69427b3
feat(library/tactic/smt/congruence_closure): make sure congruence closure module does not assign metavariables when using is_def_eq
2017-03-17 13:48:09 -07:00
Leonardo de Moura
71cd9baf7d
feat(library/type_context): add nd_is_def_eq
2017-03-17 13:47:11 -07:00
Leonardo de Moura
15c83404ee
chore(src/util/rb_tree): add more assertions to catch bugs in cmp (e.g., we provided a non transitive comparison predicate)
2017-03-17 13:47:11 -07:00
Leonardo de Moura
00e836025c
fix(library/type_context): is_def_eq_proof_irrel was not symmetric
2017-03-16 15:28:18 -07:00
Leonardo de Moura
9762fc0417
chore(src/util/rb_tree): add debugging utils
2017-03-16 14:44:09 -07:00
Leonardo de Moura
65bc3ca1eb
feat(library/type_context): allow nested tmp modes
...
TODO: The tmp_type_context class is obsolete after this change.
We should remove it.
2017-03-16 12:58:11 -07:00
Leonardo de Moura
11dcab1b31
fix(frontends/lean/elaborator): fixes #1458
2017-03-16 10:31:21 -07:00
Leonardo de Moura
22f391c0e1
feat(frontends/lean/elaborator): tolerate orphan bounded variables
...
The pretty printer is used to display ill-formed expressions,
and it uses type_context.
2017-03-16 10:22:52 -07:00
Leonardo de Moura
a897fd3f17
fix(frontends/lean): pattern matching in the declaration header
2017-03-16 01:09:12 -07:00
Leonardo de Moura
16392fda7d
chore(tests/lean/inductive_sorry): remove test
2017-03-15 20:37:53 -07:00
Daniel Selsam
cddf5f081d
fix(library/tactic/kabstract.cpp): only use replace_fn cache if replacing all occs
2017-03-15 19:40:52 -07:00
Daniel Selsam
9135e231f0
fix(tests/lean/inductive_sorry.lean): fix broken test
2017-03-15 19:40:52 -07:00
Leonardo de Moura
83fbb605f4
chore(tests/lean): fix tests
2017-03-15 19:40:52 -07:00
Leonardo de Moura
36770119b6
feat(library): do not generate C.destruct (for structures), and C.induction_on (for structures and inductive datatypes)
2017-03-15 14:45:13 -07:00
Daniel Selsam
7f56f23e70
chore(frontends/lean/inductive_cmds): allow sorrys
2017-03-15 14:06:56 -07:00
Sebastian Ullrich
e3b9190fe2
refactor(library/tactic/user_attribute): use attribute for registering attributes. naturally.
2017-03-15 14:06:34 -07:00
Sebastian Ullrich
c325438453
fix(frontends/lean/elaborator): let expr patterns
2017-03-15 14:06:08 -07:00
Sebastian Ullrich
647d7a8501
fix(frontends/lean/elaborator): expr patterns should ignore binding names
2017-03-15 14:06:00 -07:00
Leonardo de Moura
11a5f81197
test(tests/lean): add test for unification hints
2017-03-12 17:02:05 -07:00
Leonardo de Moura
abbc483246
chore(tests/lean/type_error_at_eval_expr): fix test
...
We should suppress the internal numerical ids when displaying this kind
of error message as suggested by @kha
2017-03-12 16:48:14 -07:00
Leonardo de Moura
8d409d7c63
feat(library/unification_hint): unification hint validation
2017-03-12 16:42:16 -07:00
Leonardo de Moura
e0e3f51c44
feat(library/init): add unification hint for add/succ
2017-03-12 13:45:30 -07:00
Leonardo de Moura
d1ace9e243
chore(library/unification_hint): add check
2017-03-12 12:19:12 -07:00
Leonardo de Moura
9bc378ea49
perf(library/unification_hint): improve performance
2017-03-12 12:07:51 -07:00
Leonardo de Moura
9ce9c0331f
feat(frontends/lean/elaborator): add option 'elaborator.coercion'
...
This option is available in Lean 2, but it was accidentally removed
from Lean 3.
2017-03-12 11:27:41 -07:00
Leonardo de Moura
bc7089dc70
chore(frontends/lean/elaborator): retract c58f61e
...
See discussion at #1438
2017-03-12 09:58:57 -07:00
Daniel Selsam
f3e71e52fc
feat(frontends/smt2/parser.cpp): allow tracing from the smt tactic
2017-03-12 09:54:09 -07:00
