Scrut::type-mismatch
Key: Scrut::type-mismatch
Category: elimination · Severity: error
Source: src/diag/hints.nix:866
the scrutinee's type must match the eliminator's expected shape. Annotate the scrutinee via ann, or switch to the eliminator that matches its inferred type.
Example
Hint::Scrut::type-mismatch means the Scrut position supplies a term whose type does not match the expected type. The example shows the failing form first, then one way to give the checker the missing structure.
# Bad: the eliminator is used on a scrutinee of the wrong type.
natElim motive zero succCase true_
# Better: use a scrutinee with the eliminator's type.
natElim motive zero succCase (natLit 3)