[nyssos]

> I am still profoundly confused about what the 'tactics' truly are.

They're macros: a `tactic a` is (after sanding off the implementation details) a function

    tactic_state -> Either (tactic_state, error) (tactic_state, a)

where `tactic_state` is the internal state of the elaborator.