add tactics #5
Description
- 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
thmand a proof script, that is progressively built. This way you eventually get a proof script that can replace the tactic invocation.