SigmaFst::refinement-failed
Key: SigmaFst::refinement-failed
Category: refinement · Severity: error
Source: src/diag/hints.nix:916
the first component violates the fst type's refinement predicate
Example
Hint::SigmaFst::refinement-failed means the SigmaFst 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: fst has the right base type but fails its refinement.
pair (-1) proof
# Better: fst satisfies the refinement.
pair 1 proof