1
1
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 20:51:43 +03:00
Idris2/tests/ttimp/dot001/Dot4.yaff

18 lines
425 B
Plaintext
Raw Normal View History

data Nat : Type where
Z : Nat
S : Nat -> Nat
plus : Nat -> Nat -> Nat
plus Z $y = y
plus (S $k) $y = S (plus k y)
data Baz : Nat -> Type where
AddThings : (x : Nat) -> (y : Nat) -> Baz (plus x y)
addBaz : (x : Nat) -> Baz x -> Nat
addBaz (plus x y) (AddThings _ _) = plus x y
-- Can't unify because of the repeated argument
addBaz4 : (x : Nat) -> Baz x -> Nat
addBaz4 (plus _ _) (AddThings x x) = plus x x