pub fn measure_theorem(input: &str) -> Result<usize, ParseError>Expand description
The EXTENT of the ## Theorem: block at the front of input, read from its syntax alone.
Where a block ENDS is a fact about its text; what it MEANS is a fact about the context it is
read in. A document is split into blocks before any of them runs, so its splitter can only ask
the first question: a ## To block whose equation set is over a function an EARLIER block of the
same document declares cannot be compiled yet, and it does not need to be — it is measured here,
and compiled when it is read to be run, against the context the blocks before it built. The
flat reading’s refusals of what only a context can compile (a nested pattern, a catch-all,
a second column) are skipped for the same reason: measuring them needs their syntax only.