mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-24 12:14:26 +03:00
36 lines
675 B
Idris
36 lines
675 B
Idris
|
%default total
|
||
|
|
|
||
|
|
transport : a === b -> a -> b
|
||
|
|
transport Refl x = x
|
||
|
|
|
||
|
|
transportRev : a === b -> b -> a
|
||
|
|
transportRev Refl x = x
|
||
|
|
|
||
|
|
data D : Type where
|
||
|
|
MkD : Nat -> Nat -> D
|
||
|
|
|
||
|
|
P : D -> Type
|
||
|
|
P (MkD (S _) _) = Void
|
||
|
|
P (MkD _ (S (S _))) = Void
|
||
|
|
P (MkD 0 0) = ()
|
||
|
|
P (MkD 0 1) = ()
|
||
|
|
|
||
|
|
lem : (n : Nat) -> P (MkD n (S (S m))) === Void
|
||
|
|
lem 0 = Refl
|
||
|
|
lem (S n) = Refl
|
||
|
|
|
||
|
|
mutual
|
||
|
|
f : (x : D) -> P x
|
||
|
|
-- The loop:
|
||
|
|
f (MkD (S n) _) = transport (lem n) (g (MkD n)) -- this call to g is fishy!
|
||
|
|
f (MkD n (S (S m))) = transportRev (lem n) (f (MkD (S n) m))
|
||
|
|
-- Base cases:
|
||
|
|
f (MkD 0 0) = ()
|
||
|
|
f (MkD 0 1) = ()
|
||
|
|
|
||
|
|
g : (h : Nat -> D) -> P (h 2)
|
||
|
|
g h = f (h 2)
|
||
|
|
|
||
|
|
loop : Void
|
||
|
|
loop = f (MkD 1 0)
|