mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-18 18:31:43 +03:00
a2ce8d0b7d
When we encounter them, not that they're a binding as normal, but also record the thing they expand to. Then bind as a PLet, and convert that to a Let on the RHS so it has computational force. The case tree compiler knows about as patterns, so they get compiled to use the appropriate name on the rhs (rather than a let).
20 lines
344 B
Plaintext
20 lines
344 B
Plaintext
data Nat : Type where
|
|
Z : Nat
|
|
S : Nat -> Nat
|
|
|
|
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
|