ULevel::type-mismatch
Key: ULevel::type-mismatch
Category: universe · Severity: error
Source: src/diag/hints.nix:926
the level argument of U must be a Level
Example
Hint::ULevel::type-mismatch means the ULevel 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: U expects a Level argument.
u nat
# Better: pass a level.
u level0