Motive::not-a-function
Key: Motive::not-a-function
Category: arity · Severity: error
Source: src/diag/hints.nix:868
the motive must be a function from the scrutinee's type into a type, not a bare type or value. Supply a one-argument function whose body lives in some U k.
Example
Hint::Motive::not-a-function means the Motive position uses a non-function where the checker needs a Pi-typed term. The example shows the failing form first, then one way to give the checker the missing structure.
# Bad: an eliminator motive is a bare type.
natElim nat zero succCase n
# Better: make the motive a function from the scrutinee.
natElim (x: nat) zero succCase n