Tests for ModuleExpressions #
Smoke tests for the moduletyping, normalmodule and reduce_simp tactics, kept out of
ModuleExpressions.lean so that file stays definitions-and-proofs only.
Smoke tests #
Smoke tests #
reduce_simp_head smoke tests #
Written as ∃ m, reduce x = m, proved by ⟨_, by reduce_simp_head⟩: the witness _ is a
genuine metavariable the tactic assigns via unification, unlike example : reduce x = _ := ...
directly (there, the _ sits in the stated type, which Lean fully elaborates — including
resolving its own holes — before the tactic block ever runs, so it can't be left for the tactic
to fill; confirmed empirically, "don't know how to synthesize placeholder"). The anonymous
constructor's fields, by contrast, are genuinely elaborated together with the tactic proof.