- tactics are mostly in rust - bridge to meta-language (where a tactic can be "applied" like a function or other builtins; composition operators) - return a `thm` *and* a proof script, that is progressively built. This way you eventually get a proof script that can replace the tactic invocation.
thmand a proof script, that is progressively built. This way you eventually get a proof script that can replace the tactic invocation.