## Stream: new members

### Topic: extracting tactics and proof terms

#### 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