1
{-# OPTIONS -v tc.polarity.set:10 #-}
3
{-# OPTIONS --sized-types #-}
4
module DataPolarity where
6
open import Common.Size
8
data Nat : {size : Size} -> Set where
9
zero : {size : Size} -> Nat {↑ size}
10
suc : {size : Size} -> Nat {size} -> Nat {↑ size}
12
data Pair (A : Set) : Set where
13
_,_ : A -> A -> Pair A
15
split : {i : Size} → Nat {i} → Pair (Nat {i})
16
split zero = zero , zero
17
split (suc n) with split n
18
... | (l , r) = suc r , l
20
MyPair : Nat → Set → Set
21
MyPair zero A = Pair A
22
MyPair (suc n) A = MyPair n A
24
mysplit : {i : Size} → (n : Nat {i}) → MyPair (suc zero) (Nat {i})
25
mysplit zero = zero , zero
26
mysplit (suc n) with mysplit n
27
... | (l , r) = suc r , l