git.iko.soy/Idris-dev
on aa42f71 help sign in
Idris-dev/lib/Data/Vect.idr
32 lines 1.2 kB history raw
1module Data.Vect
3import Language.Reflection
5%access public
6%default total
8--------------------------------------------------------------------------------
9-- Elem
10--------------------------------------------------------------------------------
12data Elem : a -> Vect a k -> Type where
13 Here : {xs : Vect a k} -> Elem x (x::xs)
14 There : {xs : Vect a k} -> Elem x xs -> Elem x (y::xs)
16findElem : Nat -> List (TTName, Binder TT) -> TT -> Tactic
17findElem O ctxt goal = Refine "Here" `Seq` Solve
18findElem (S n) ctxt goal = GoalType "Elem" (Try (Refine "Here" `Seq` Solve) (Refine "There" `Seq` (Solve `Seq` findElem n ctxt goal)))
20replaceElem : (xs : Vect t k) -> Elem x xs -> (y : t) -> (ys : Vect t k ** Elem y ys)
21replaceElem (x::xs) Here y = (y :: xs ** Here)
22replaceElem (x::xs) (There xinxs) y with (replaceElem xs xinxs y)
23 | (ys ** yinys) = (x :: ys ** There yinys)
25replaceByElem : (xs : Vect t k) -> Elem x xs -> t -> Vect t k
26replaceByElem (x::xs) Here y = y :: xs
27replaceByElem (x::xs) (There xinxs) y = x :: replaceByElem xs xinxs y
29mapElem : {xs : Vect t k} -> {f : t -> u} -> Elem x xs -> Elem (f x) (map f xs)
30mapElem Here = Here
31mapElem (There e) = There (mapElem e)