pub struct CompileReport {
pub unreachable_clauses: Vec<usize>,
}Expand description
What the compiler noticed on the way through, beyond the term itself.
Fields§
§unreachable_clauses: Vec<usize>Clause indices no input can ever select, because an earlier clause already covers everything they do. First-match semantics makes them dead rather than wrong, so this is information for the surface to surface.
★ WHAT LEAN DOES WITH THE SAME FACT, and it is not what the previous sentence here
claimed. Lean does NOT quietly accept a redundant alternative: Lean/Elab/Match.lean:999
calls logError "redundant alternative" for every index in result.unusedAltIdxs, and
the run on this box confirms it — def h : Hue → Bool | .ruby => true | .jade => false | _ => true answers error: redundant alternative. The error is non-fatal (#eval h Hue.ruby still prints true, so the declaration is added), and
Lean/Elab/Match.lean:985-988 declares the option that turns it off:
match.ignoreUnusedAlts, default false.
So the MEANING is the same in both compilers and only the default severity differs: LOGOS
behaves as Lean does under set_option match.ignoreUnusedAlts true. What is still missing
is the report reaching a reader — literate_parser::parse_consider discards this census,
so a dead clause is silent rather than merely non-fatal. That needs a warning channel on
Command, which this module does not own.
Trait Implementations§
Source§impl Clone for CompileReport
impl Clone for CompileReport
Source§fn clone(&self) -> CompileReport
fn clone(&self) -> CompileReport
1.0.0 · Source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
source. Read more