2020-05-19 20:25:18 +03:00
|
|
|
import Data.Vect
|
|
|
|
|
|
|
|
|
|
%unbound_implicits off
|
|
|
|
|
|
|
|
|
|
append : forall n, m, a . Vect n a -> Vect m a -> Vect (n + m) a
|
2021-01-16 10:03:45 +03:00
|
|
|
append [] ys = ys
|
2020-05-19 20:25:18 +03:00
|
|
|
append (x :: xs) ys = x :: append xs ys
|
|
|
|
|
|
|
|
|
|
data Env : forall n . Vect n Type -> Type where
|
|
|
|
|
ENil : Env []
|
|
|
|
|
ECons : forall t, ts . t -> Env ts -> Env (t :: ts)
|
|
|
|
|
|
|
|
|
|
-- fine because the only name used in bound, and it'll infer types for
|
|
|
|
|
-- xs and its indices
|
|
|
|
|
len : forall xs . Env xs -> Nat
|
|
|
|
|
|
|
|
|
|
-- neither of these are fine
|
|
|
|
|
len': Env xs -> Nat
|
|
|
|
|
append' : Vect n a -> Vect m a -> Vect (n + m) a
|
