mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2025-01-08 06:07:11 +03:00
ea0de3d499
It's not quite there yet, though, because the treatment of 'as' patterns isn't quite right and the slightly hacky approach we're taking might not be the best. Rethinking now...
23 lines
386 B
Plaintext
23 lines
386 B
Plaintext
data Nat : Type where
|
|
Z : Nat
|
|
S : Nat -> Nat
|
|
|
|
simpleAs : Nat -> Nat
|
|
simpleAs z@(_) = z
|
|
|
|
as : Nat -> Nat
|
|
as Z = Z
|
|
as p@(S $k) = p
|
|
|
|
plus : Nat -> Nat -> Nat
|
|
plus Z $y = y
|
|
plus (S $k) $y = S (plus k y)
|
|
|
|
data PairNat : Type where
|
|
MkPair : Nat -> Nat -> PairNat
|
|
|
|
pairPred : Nat -> PairNat
|
|
pairPred Z = MkPair Z Z
|
|
pairPred (S Z) = MkPair Z Z
|
|
pairPred (S p@(S $k)) = MkPair p k
|