git.iko.soy/Idris-dev
on master help sign in
Binder name changes in Elem/There
e55fe2fEdwin Brady
libs/base/Data/List.idr+1−1
compare with master
unifiedsplit
@@ -13,7 +13,7 @@ data Elem : a -> List a -> Type where
13 ||| A proof that the element is after the front of the list
13 ||| A proof that the element is after the front of the list
14 |||
14 |||
15 ||| Example: `the (Elem "b" ["a", "b"]) (There Here)`
15 ||| Example: `the (Elem "b" ["a", "b"]) (There Here)`
16− There : Elem x xs -> Elem x (y :: xs)
16+ There : (later : Elem x xs) -> Elem x (y :: xs)
17
17
18implementation Uninhabited (Elem {a} x []) where
18implementation Uninhabited (Elem {a} x []) where
19 uninhabited Here impossible
19 uninhabited Here impossible
libs/base/Data/Vect.idr+1−1
@@ -573,7 +573,7 @@ implementation DecEq a => DecEq (Vect n a) where
573||| A proof that some element is found in a vector
573||| A proof that some element is found in a vector
574data Elem : a -> Vect k a -> Type where
574data Elem : a -> Vect k a -> Type where
575 Here : Elem x (x::xs)
575 Here : Elem x (x::xs)
576− There : (prf : Elem x xs) -> Elem x (y::xs)
576+ There : (later : Elem x xs) -> Elem x (y::xs)
577
577
578||| Nothing can be in an empty Vect
578||| Nothing can be in an empty Vect
579noEmptyElem : {x : a} -> Elem x [] -> Void
579noEmptyElem : {x : a} -> Elem x [] -> Void