LevelSucPred::type-mismatch
Key: LevelSucPred::type-mismatch
Category: universe · Severity: error
Source: src/diag/hints.nix:920
the predecessor of suc must be a Level
Example
Hint::LevelSucPred::type-mismatch means the LevelSucPred 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: suc expects a Level.
levelSuc nat
# Better: pass a level expression.
levelSuc level0