mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-27 05:34:40 +03:00
32 lines
642 B
Plaintext
32 lines
642 B
Plaintext
|
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 Eq : $a -> $b -> Type where
|
||
|
|
Refl : Eq $x $x
|
||
|
|
|
||
|
|
data Test : Type where
|
||
|
|
MkTest : Integer -> Integer -> Test
|
||
|
|
|
||
|
|
eqTest : Eq (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))
|
||
|
|
eqTest = Refl
|
||
|
|
|
||
|
|
etaGood1 : Eq MkTest (\x => \y => MkTest ? ?)
|
||
|
|
etaGood1 = Refl
|
||
|
|
|
||
|
|
etaGood1b : Eq (\x => \y => MkTest ? ?) MkTest
|
||
|
|
etaGood1b = Refl
|
||
|
|
|
||
|
|
etaGood2: Eq (MkTest 1) (\x => MkTest ? x)
|
||
|
|
etaGood2 = Refl
|
||
|
|
|
||
|
|
etaGood3: (f : $a -> $b) -> Eq f (\x => f x)
|
||
|
|
etaGood3 $f = Refl
|
||
|
|
|
||
|
|
-- etaBad : Eq MkTest (\x : Char => \y => MkTest ? ?)
|
||
|
|
-- etaBad = Refl
|