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