pub const ANONYMOUS_SECTION: &str = "an anonymous section";Expand description
How an ANONYMOUS section is named in a report. Lean’s section may be written with no name at
all, and a scope with no name still has to be reportable — as an unclosed scope at the end of a
document, and as the scope a mismatched End failed to close.