c52be7e8c5
@kha, I added autocompletion for ^. I try to elaborate the expression
before ^. using the local context provided by the parser.
The autocompletion only works if the type for the expression before ^. can be
inferred. This is a big limitation because this information cannot be
obtained in many cases. Here are examples that do not work:
meta def proof_for (e : expr) : smt_tactic expr :=
do cc ← to_cc_state, cc^.proof_for e
--^ does not work here
If we annotate cc with its type, it works:
meta def proof_for (e : expr) : smt_tactic expr :=
do cc : cc_state ← to_cc_state, cc^.proof_for e
--^ works
We don't have typing information on the equation lhs at
autocompletion time. So, the following will not work
private meta def mk_smt_goals_for (cfg : smt_config)
: list expr → list smt_goal → list expr → tactic (list smt_goal × list expr)
| [] sr tr := return (sr^.reverse, tr^.reverse)
--^ does not work since
| (tg::tgs) sr tr := ...
9 lines
4.1 KiB
Text
9 lines
4.1 KiB
Text
{"msg":{"caption":"","file_name":"f","pos_col":14,"pos_line":4,"severity":"error","text":"invalid '~>' notation, 'l' is not a valid \"field\" because environment does not contain 'and.l'\n h y\nwhich has type\n p y ∧ q y"},"response":"additional_message"}
|
|
{"msg":{"caption":"","file_name":"f","pos_col":14,"pos_line":8,"severity":"error","text":"invalid '~>' notation, 'le' is not a valid \"field\" because environment does not contain 'and.le'\n h y\nwhich has type\n p y ∧ q y"},"response":"additional_message"}
|
|
{"msg":{"caption":"","file_name":"f","pos_col":14,"pos_line":12,"severity":"error","text":"invalid '~>' notation, 'r' is not a valid \"field\" because environment does not contain 'and.r'\n h y\nwhich has type\n p y ∧ q y"},"response":"additional_message"}
|
|
{"msg":{"caption":"","file_name":"f","pos_col":39,"pos_line":17,"severity":"error","text":"invalid '~>' notation, identifier or numeral expected"},"response":"additional_message"}
|
|
{"message":"file invalidated","response":"ok","seq_num":0}
|
|
{"completions":[{"source":{"column":4,"file":"/library/init/core.lean","line":115},"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":419},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"}],"prefix":"l","response":"ok","seq_num":5}
|
|
{"completions":[{"source":{"column":4,"file":"/library/init/core.lean","line":115},"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":419},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"}],"prefix":"le","response":"ok","seq_num":9}
|
|
{"completions":[{"source":{"column":10,"file":"/library/init/core.lean","line":109},"text":"rec","type":"(?a → ?b → ?C) → ?a ∧ ?b → ?C"},{"source":{"column":10,"file":"/library/init/core.lean","line":109},"text":"rec_on","type":"?a ∧ ?b → (?a → ?b → ?C) → ?C"},{"source":{"column":4,"file":"/library/init/core.lean","line":120},"text":"right","type":"?a ∧ ?b → ?b"}],"prefix":"r","response":"ok","seq_num":13}
|
|
{"completions":[{"source":{"column":14,"file":"/library/init/logic.lean","line":412},"text":"assoc","type":"(?a ∧ ?b) ∧ ?c ↔ ?a ∧ ?b ∧ ?c"},{"source":{"column":10,"file":"/library/init/core.lean","line":109},"text":"cases_on","type":"?a ∧ ?b → (?a → ?b → ?C) → ?C"},{"source":{"column":14,"file":"/library/init/logic.lean","line":407},"text":"comm","type":"?a ∧ ?b ↔ ?b ∧ ?a"},{"source":{"column":11,"file":"/library/init/logic.lean","line":665},"text":"decidable","type":"decidable (?p ∧ ?q)"},{"source":{"column":6,"file":"/library/init/logic.lean","line":216},"text":"elim","type":"?a ∧ ?b → (?a → ?b → ?c) → ?c"},{"source":{"column":4,"file":"/library/init/core.lean","line":112},"text":"elim_left","type":"?a ∧ ?b → ?a"},{"source":{"column":4,"file":"/library/init/core.lean","line":117},"text":"elim_right","type":"?a ∧ ?b → ?b"},{"source":{"column":6,"file":"/library/init/logic.lean","line":394},"text":"imp","type":"(?a → ?c) → (?b → ?d) → ?a ∧ ?b → ?c ∧ ?d"},{"source":{"column":10,"file":"/library/init/core.lean","line":109},"text":"induction_on","type":"?a ∧ ?b → (?a → ?b → ?C) → ?C"},{"source":{"column":10,"file":"/library/init/core.lean","line":109},"text":"intro","type":"?a → ?b → ?a ∧ ?b"},{"source":{"column":4,"file":"/library/init/core.lean","line":115},"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":419},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"},{"source":{"column":10,"file":"/library/init/core.lean","line":109},"text":"rec","type":"(?a → ?b → ?C) → ?a ∧ ?b → ?C"},{"source":{"column":10,"file":"/library/init/core.lean","line":109},"text":"rec_on","type":"?a ∧ ?b → (?a → ?b → ?C) → ?C"},{"source":{"column":4,"file":"/library/init/core.lean","line":120},"text":"right","type":"?a ∧ ?b → ?b"},{"source":{"column":6,"file":"/library/init/logic.lean","line":219},"text":"swap","type":"?a ∧ ?b → ?b ∧ ?a"},{"source":{"column":4,"file":"/library/init/logic.lean","line":222},"text":"symm","type":"?a ∧ ?b → ?b ∧ ?a"}],"prefix":"","response":"ok","seq_num":17}
|