Binder name changes in Elem/There
commite55fe2fa98e1ebfc41e6c0153f4377064069ef74
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateFri 5 Feb 2016, 14:44 (11 years ago)
parent2a6b577
libs/base/Data/List.idr+1−1
@@ -13,7 +13,7 @@ data Elem : a -> List a -> Type where
1313 ||| A proof that the element is after the front of the list
1414 |||
1515 ||| 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)
1717
1818implementation Uninhabited (Elem {a} x []) where
1919 uninhabited Here impossible
libs/base/Data/Vect.idr+1−1
@@ -573,7 +573,7 @@ implementation DecEq a => DecEq (Vect n a) where
573573||| A proof that some element is found in a vector
574574data Elem : a -> Vect k a -> Type where
575575 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)
577577
578578||| Nothing can be in an empty Vect
579579noEmptyElem : {x : a} -> Elem x [] -> Void