pub const ANON_CTOR_MARKER: &str = "⟨anon⟩";Expand description
Reserved head marking a surface anonymous constructor ⟨e₁, …, eₙ⟩ (E3). The parser
emits ⟨anon⟩ e₁ … eₙ; the elaborator (this module) rewrites it to the sole constructor
of the expected inductive and then discards the marker — it NEVER reaches a kernel term.
The name contains ⟨/⟩, characters the identifier lexer cannot produce, so it can
never collide with a user global. Like the ?-prefixed metavariables above, this rides
on the existing Term with no new variant.