LevelMaxLhs::type-mismatch
Key: LevelMaxLhs::type-mismatch
Category: universe · Severity: error
Source: src/diag/hints.nix:922
the left operand of max must be a Level
Example
Hint::LevelMaxLhs::type-mismatch means the LevelMaxLhs 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: max's left operand is not a Level.
levelMax nat level0
# Better: both operands are levels.
levelMax level0 level1