Stream: new members
Michael Jendrusch (Nov 12 2018 at 10:25):
This is probably a question with a simple answer, but I'll ask it either way. Is there a way to programmatically extract the sequence of tactics used to prove a given lemma? I can get the proof term pretty easily by doing something like this:
import tactic open tactic.interactive namespace my_namespace lemma my_lemma : Π n : ℕ, n + 1 > n := begin intros, rw gt, simp, comp_val, end #eval do env ← tactic.get_env, ml ← env.get(mk_str_name "my_namespace" "my_lemma"), fmt ← tactic_format_expr ml.value, trace $ "type : " ++ (to_string $ expr.to_raw_fmt ml.type) ++ "\n", trace $ "value : " ++ (to_string $ expr.to_raw_fmt ml.value) ++ "\n", return unit.star end my_namespace
but I haven't had any luck extracting tactics yet. On another note, is there some function other than
expr.to_raw_fmt for serializing expressions?
Mario Carneiro (Nov 12 2018 at 10:36):
No. It's not stored
Keeley Hoek (Nov 12 2018 at 10:41):
What do you mean "serializing"?
Michael Jendrusch (Nov 12 2018 at 11:29):
Serializing, as in generating some text (s-expression, JSON) or binary representation of expressions which can be read from another program. But I suppose
expr.to_raw_fmtshould be enough for my purposes.
Last updated: May 08 2021 at 19:11 UTC