Module tactic_script 

A tiny proof-script language over the crate::tactic combinators — proofs as TEXT, the way a Lean/Coq proof reads. This is the self-contained seam toward a full English vernacular: it has no dependency on the surface language, so it compiles a script string straight into a composed Tactic.

Grammar (precedence low → high):

script  := seq
seq     := chain (';' chain)*          // run in order
chain   := atom ('<;>' atom)*          // `t1 <;> t2`: t2 on every goal t1 spawns
atom    := '(' script ')'
         | 'first' '[' script ('|' script)* ']'   // first that applies (backtracks)
         | 'try' atom                              // run if it applies, else no-op
         | 'repeat' atom                           // apply until it stops applying
         | NAME ARG?                               // a primitive tactic

Primitive tactics: intro h, exact h, cases h, rewrite h, exists W, assumption, split, left, right, auto, induction.

Structs

ScriptError

A script parse error, with a human-readable reason.

ScriptedTheorem

One theorem of a scripted library: proved from its own premises plus the conclusions of the theorems it cites, by running script to a kernel-checked proof. The unit the prove_scripted_library driver discharges in citation order.

TacticEnv

A registry of USER-DEFINED tactics (M) — the metaprogramming seam. A user names a composite tactic (built from primitives and combinators) with TacticEnv::define, and may then reference it BY NAME in any later script, including from within other user-defined tactics. This is “write your own tactic in the language”, without Rust — the definitions are stored as source and re-expanded (depth-bounded, so a recursive definition is rejected rather than looping) wherever the name appears.

Functions

parse_script

Compile a proof-script string into a composed Tactic (no user-defined tactics).

parse_script_with_env

Compile a proof-script string with USER-DEFINED tactics resolved from env (M).

prove_scripted_library

Discharge a library of scripted theorems in citation order, on a shared axioms base. Each theorem is proved by its ScriptedTheorem::script from its premises, the axioms, and the conclusions of the theorems it cites (already proved); a proved conclusion becomes a citable lemma for later theorems — the scraped-Euclid-graph discipline, now driven by tactic scripts. Results come back in INPUT order.