mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-26 13:11:30 +03:00
6d96341776
Rather than returning a complete list of results, return a pair of the first result, and a continuation. The continuation explains how to continue the search if the given result is deemed unacceptable (either on encountering an error somewhere, or just if the caller wants the next result). This means we don't search needlessly if we're only looking for the first result. Fixes #228
36 lines
821 B
Idris
36 lines
821 B
Idris
data Vect : Nat -> Type -> Type where
|
|
Nil : Vect Z a
|
|
(::) : a -> Vect k a -> Vect (S k) a
|
|
|
|
%name Vect xs, ys, zs
|
|
|
|
my_cong : forall f . (x : a) -> (y : a) -> x = y -> f x = f y
|
|
|
|
my_curry : ((a, b) -> c) -> a -> b -> c
|
|
|
|
my_uncurry : (a -> b -> c) -> (a, b) -> c
|
|
|
|
append : Vect n a -> Vect m a -> Vect (n + m) a
|
|
|
|
lappend : (1 xs : List a) -> (1 ys : List a) -> List a
|
|
|
|
zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
|
|
|
|
data Env : Vect n Type -> Type where
|
|
ENil : Env []
|
|
ECons : a -> Env xs -> Env (a :: xs)
|
|
|
|
%name Env es
|
|
|
|
data Elem : a -> Vect n a -> Type where
|
|
Here : Elem x (x :: xs)
|
|
There : (p : Elem x xs) -> Elem x (y :: xs)
|
|
|
|
lookup : Elem ty vs -> Env vs -> ty
|
|
|
|
data Tree : (a : Type) -> Type where
|
|
Leaf : a -> Tree a
|
|
Node : a -> Tree a -> Tree a -> Tree a
|
|
|
|
foo : Tree Nat
|