mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-14 03:14:14 +03:00
16 lines
277 B
Idris
16 lines
277 B
Idris
data MyNat = MyO | MyS MyNat
|
|
|
|
%default total
|
|
|
|
data Bad = MkBad (Bad -> Int) Int
|
|
| MkBad' Int
|
|
|
|
vapp : Vect n a -> Vect m a -> Vect (n + m) a
|
|
vapp [] ys = ys
|
|
vapp (x :: xs) ys = x :: vapp xs ys
|
|
|
|
foo : Bad -> Int
|
|
foo (MkBad f i) = f (MkBad' i)
|
|
foo (MkBad' x) = x
|
|
|