Navigation

MuDesc::not-a-desc

Key: MuDesc::not-a-desc

Category: description · Severity: error

Source: src/diag/hints.nix:864

the description argument of μ must be a Desc I term, not an ordinary value. Construct it with descRet, descArg, descRec, descPi, or descPlus.

Example

Hint::MuDesc::not-a-desc means the MuDesc position uses an ordinary term where the checker needs a Desc. The example shows the failing form first, then one way to give the checker the missing structure.

# Bad: mu expects a Desc, not a term.
mu nat (natLit 0)

# Better: construct the Desc explicitly.
mu nat (descRet zero)

← All diagnostic hints