SigmaSnd::refinement-failed
Key: SigmaSnd::refinement-failed
Category: refinement · Severity: error
Source: src/diag/hints.nix:918
the second component violates the snd type's refinement predicate
Example
Hint::SigmaSnd::refinement-failed means the SigmaSnd position contains a value that fails the refinement predicate. The example shows the failing form first, then one way to give the checker the missing structure.
# Bad: snd fails the refinement depending on fst.
pair 3 (-1)
# Better: snd satisfies the dependent refinement.
pair 3 4