mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-17 00:10:31 +03:00
31 lines
754 B
Idris
31 lines
754 B
Idris
module With
|
|
|
|
f : (n : Nat) -> (m : Nat ** n : Nat ** m = n + n)
|
|
f n with (n + n) proof eq
|
|
f n | Z = (Z ** n ** sym eq)
|
|
f n | (S m) = (S m ** n ** sym eq)
|
|
|
|
g : List a -> Nat
|
|
g [] = Z
|
|
g (a :: as) with (as ++ as)
|
|
g (b :: bs) | asas = Z
|
|
|
|
nested : Nat -> Nat
|
|
nested m with (m)
|
|
nested m | Z with (m + m)
|
|
nested m | Z | 0 = 1
|
|
nested m | Z | S k with (k + k)
|
|
nested m | Z | S k | Z = 2
|
|
nested m | Z | S k | S l with (l + l)
|
|
nested m | Z | S k | S l | Z = 3
|
|
nested m | Z | S k | S l | S p = 4
|
|
nested m | S k = 5
|
|
|
|
data ANat : Nat -> Type where
|
|
MkANat : (n : Nat) -> ANat n
|
|
|
|
someNats : Nat -> Nat
|
|
someNats n with (MkANat n)
|
|
someNats n | m@(MkANat n) with (MkANat n)
|
|
someNats n | p@(MkANat n) | MkANat n = Z
|