mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-21 10:41:59 +03:00
32 lines
863 B
Idris
32 lines
863 B
Idris
|
|
||
|
|
------------- Example 1 ----------------
|
||
|
|
natInjective : (x, y : Nat) -> S x === S y -> x === y
|
||
|
|
natInjective x x Refl = Refl
|
||
|
|
|
||
|
|
succNotZero : (x : Nat) -> Not (S x === Z)
|
||
|
|
succNotZero x Refl impossible
|
||
|
|
|
||
|
|
peanoNat : (a : Type
|
||
|
|
** n0 : a
|
||
|
|
** ns : a -> a
|
||
|
|
** inj : ((x, y : a) -> ns x === ns y -> x === y)
|
||
|
|
** (x : a) -> Not (ns x === n0))
|
||
|
|
peanoNat = MkDPair
|
||
|
|
Nat
|
||
|
|
$ MkDPair
|
||
|
|
Z
|
||
|
|
$ MkDPair -- {a = Nat -> Nat}
|
||
|
|
S
|
||
|
|
$ MkDPair
|
||
|
|
natInjective
|
||
|
|
succNotZero
|
||
|
|
|
||
|
|
------------- Example 2 ----------------
|
||
|
|
ac : forall r. ((x : a) -> (y : b ** r x y)) -> (f : a -> b ** (x : a) -> r x (f x))
|
||
|
|
ac g = (\x => fst (g x) ** \x => snd (g x))
|
||
|
|
|
||
|
|
------------- Example 3 ----------------
|
||
|
|
idid1 : forall A. (f : A -> A ** (x : A) -> f x = x)
|
||
|
|
idid1 = MkDPair id (\x => Refl)
|
||
|
|
|