The positivity checker complains about the definition of Nat in the following code:
data Unit : Set where tt : Unit FUN : Set₁ FUN = Set → Set Id : Unit → FUN Id tt A = A data Nat : Set where zero : Nat suc : (x : Unit) → Id x Nat → Nat -- 10,1-12,36: error: [NotStrictlyPositive] -- Nat is not strictly positive, because it occurs -- in the second argument of Id -- in the type of the constructor suc -- in the definition of Nat.
If we inline FUN in the type of Id, then Nat passes positivity check:
Id : Unit → Set → Set Id tt A = A data Nat : Set where zero : Nat suc : (x : Unit) → Id x Nat → Nat -- OK
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4