mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-01 09:49:24 +03:00
a972778eab
They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
70 lines
1.8 KiB
Plaintext
70 lines
1.8 KiB
Plaintext
data Nat : Type where
|
|
Z : Nat
|
|
S : Nat -> Nat
|
|
|
|
the : (a : Type) -> a -> a
|
|
the _ $x = x
|
|
|
|
namespace List
|
|
public export
|
|
data List : Type -> Type where
|
|
Nil : List $a
|
|
Cons : $a -> List $a -> List $a
|
|
|
|
public export
|
|
length : List $a -> Nat
|
|
length Nil = Z
|
|
length (Cons $x $xs) = S (length xs)
|
|
|
|
namespace Vect
|
|
public export
|
|
data Vect : ? -> Type -> Type where
|
|
Nil : Vect Z $a
|
|
Cons : $a -> Vect $k $a -> Vect (S $k) $a
|
|
|
|
public export
|
|
length : Vect $n $a -> Nat
|
|
length Nil = Z
|
|
length (Cons $x $xs) = S (length xs)
|
|
|
|
testList : List Integer
|
|
testList = Cons 1 (Cons 2 (Cons 3 Nil))
|
|
|
|
testVect : Vect ? Integer
|
|
testVect = Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)))
|
|
|
|
data IsType : $a -> Type -> Type where
|
|
ItIs : {x : $a} -> IsType x $a
|
|
|
|
foo : IsType 5 Integer
|
|
foo = ItIs
|
|
|
|
revapply : $arg -> ($arg -> $b) -> $b
|
|
revapply $x $f = f x
|
|
|
|
-- Testing delayed elaboration; we can't check the list until we know
|
|
-- whether it's List or Vect, which we work out from the second argument
|
|
test : Integer -> Nat
|
|
test $x = revapply (Cons x (Cons x Nil)) Vect.length
|
|
|
|
data Infer : Type where
|
|
MkInfer : $a -> Infer
|
|
|
|
long : Infer
|
|
long
|
|
= MkInfer (Vect.Cons 0 (Cons 0 (Cons 0 (Cons 0 (Cons 0 (
|
|
Cons 0 (Cons 0 (Cons 0 (Cons 0 (Cons 0 (
|
|
Cons 0 (Cons 0 (Cons 0 (Cons 0 (Cons 0 (
|
|
Cons 0 (Cons 0 (Cons 0 (Cons 0 (Cons 0 (
|
|
Cons 0 (Cons 0 (Cons 0 (Cons 0 (Cons 0 (
|
|
Cons 0 (Cons 0 (Cons 0 (Cons 0 (Cons 0 (
|
|
Cons 0 (Cons 0 (Cons 0 (Cons 0 (Cons 0 (
|
|
Cons 0 (Cons 0 (Cons 0 (Cons 0 (Cons 0 (
|
|
Cons 0 (Cons 0 (Cons 0 (Cons 0 (Cons 0 (
|
|
Cons 0 (Cons 0 (Cons 0 (Cons 0 (Cons 0 (
|
|
Cons 0 (Cons 0 (Cons 0 (Cons 0 (Cons 0 (
|
|
Cons 0 (Cons 0 (Cons 0 (Cons 0 (Cons 0 (
|
|
Cons 0 (Cons 0 (Cons 0 (Cons 0 (Cons 0 (
|
|
Nil)))))))))))))))))))))))))))))))))))
|
|
)))))))))))))))))))))))))))))))
|