1
{-# OPTIONS --experimental-irrelevance #-}
2
module MatchOnIrrelevantData1 where
9
data Fin : Nat -> Set where
10
zero : (n : Nat) -> Fin (suc n)
11
suc : (n : Nat) -> Fin n -> Fin (suc n)
13
toNat : (n : Nat) → .(Fin n) -> Nat
14
toNat (suc n) (zero .n) = zero
15
toNat (suc n) (suc .n i) = suc (toNat n i)