lib/Data/Vect.idr · Idris-dev

git.iko.soy/Idris-dev

on d9c3c21 help sign in

33 lines 1.2 kB history raw

1module Data.Vect

3import Language.Reflection

5%access public

6%default total

8--------------------------------------------------------------------------------

9-- Elem

10--------------------------------------------------------------------------------

12using (xs : Vect k a)

13 data Elem : a -> Vect k a -> Type where

14 Here : Elem x (x::xs)

15 There : Elem x xs -> Elem x (y::xs)

17findElem : Nat -> List (TTName, Binder TT) -> TT -> Tactic

18findElem Z ctxt goal = Refine "Here" `Seq` Solve

19findElem (S n) ctxt goal = GoalType "Elem" (Try (Refine "Here" `Seq` Solve) (Refine "There" `Seq` (Solve `Seq` findElem n ctxt goal)))

21replaceElem : (xs : Vect k t) -> Elem x xs -> (y : t) -> (ys : Vect k t ** Elem y ys)

22replaceElem (x::xs) Here y = (y :: xs ** Here)

23replaceElem (x::xs) (There xinxs) y with (replaceElem xs xinxs y)

24 | (ys ** yinys) = (x :: ys ** There yinys)

26replaceByElem : (xs : Vect k t) -> Elem x xs -> t -> Vect k t

27replaceByElem (x::xs) Here y = y :: xs

28replaceByElem (x::xs) (There xinxs) y = x :: replaceByElem xs xinxs y

30mapElem : {xs : Vect k t} -> {f : t -> u} -> Elem x xs -> Elem (f x) (map f xs)

31mapElem Here = Here

32mapElem (There e) = There (mapElem e)