git.iko.soy/Idris-dev
on master help sign in
Remove some needless 'using' blocks
505905dEdwin Brady
libs/base/Data/HVect.idr+2−2
compare with master
unifiedsplit
@@ -17,7 +17,7 @@ using (k : Nat, ts : Vect k Type)
17 index fZ (x::xs) = x
17 index fZ (x::xs) = x
18 index (fS j) (x::xs) = index j xs
18 index (fS j) (x::xs) = index j xs
19
19
20− deleteAt : {us : Vect (S l) Type} -> (i : Fin (S l)) -> HVect us -> HVect (deleteAt i us)
20+ deleteAt : (i : Fin (S l)) -> HVect us -> HVect (deleteAt i us)
21 deleteAt fZ (x::xs) = xs
21 deleteAt fZ (x::xs) = xs
22 deleteAt {l = S m} (fS j) (x::xs) = x :: deleteAt j xs
22 deleteAt {l = S m} (fS j) (x::xs) = x :: deleteAt j xs
23 deleteAt {l = Z} (fS j) (x::xs) = absurd j
23 deleteAt {l = Z} (fS j) (x::xs) = absurd j
@@ -32,7 +32,7 @@ using (k : Nat, ts : Vect k Type)
32 updateAt (fS j) f (x::xs) = x :: updateAt j f xs
32 updateAt (fS j) f (x::xs) = x :: updateAt j f xs
33
33
34 ||| Append two `HVect`s.
34 ||| Append two `HVect`s.
35− (++) : {us : Vect l Type} -> HVect ts -> HVect us -> HVect (ts ++ us)
35+ (++) : HVect ts -> HVect us -> HVect (ts ++ us)
36 (++) [] ys = ys
36 (++) [] ys = ys
37 (++) (x::xs) ys = x :: (xs ++ ys)
37 (++) (x::xs) ys = x :: (xs ++ ys)
38
38
libs/base/Data/List.idr+24−25
@@ -2,30 +2,29 @@ module Data.List
2
2
3%access public
3%access public
4
4
5−using (xs : List a)
6− ||| A proof that some element is found in a list
5+||| A proof that some element is found in a list
7− data Elem : a -> List a -> Type where
6+data Elem : a -> List a -> Type where
8− Here : Elem x (x :: xs)
7+ Here : Elem x (x :: xs)
9− There : Elem x xs -> Elem x (y :: xs)
8+ There : Elem x xs -> Elem x (y :: xs)
10
9
11− instance Uninhabited (Elem {a} x []) where
10+instance Uninhabited (Elem {a} x []) where
12− uninhabited Here impossible
11+ uninhabited Here impossible
13− uninhabited (There p) impossible
12+ uninhabited (There p) impossible
14
13
15− ||| Is the given element a member of the given list.
14+||| Is the given element a member of the given list.
16− |||
15+|||
17− ||| @x The element to be tested.
16+||| @x The element to be tested.
18− ||| @xs The list to be checked against
17+||| @xs The list to be checked against
19− isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)
18+isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)
20− isElem x [] = No absurd
19+isElem x [] = No absurd
21− isElem x (y :: xs) with (decEq x y)
20+isElem x (y :: xs) with (decEq x y)
22− isElem x (x :: xs) | (Yes refl) = Yes Here
21+ isElem x (x :: xs) | (Yes refl) = Yes Here
23− isElem x (y :: xs) | (No contra) with (isElem x xs)
22+ isElem x (y :: xs) | (No contra) with (isElem x xs)
24− isElem x (y :: xs) | (No contra) | (Yes prf) = Yes (There prf)
23+ isElem x (y :: xs) | (No contra) | (Yes prf) = Yes (There prf)
25− isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)
24+ isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)
26− where
25+ where
27− mkNo : {xs' : List a} ->
26+ mkNo : {xs' : List a} ->
28− ((x' = y') -> _|_) -> (Elem x' xs' -> _|_) ->
27+ ((x' = y') -> _|_) -> (Elem x' xs' -> _|_) ->
29− Elem x' (y' :: xs') -> _|_
28+ Elem x' (y' :: xs') -> _|_
30− mkNo f g Here = f refl
29+ mkNo f g Here = f refl
31− mkNo f g (There x) = g x
30+ mkNo f g (There x) = g x
libs/base/Data/Vect.idr+4−5
@@ -9,11 +9,10 @@ import Language.Reflection
9-- Elem
9-- Elem
10--------------------------------------------------------------------------------
10--------------------------------------------------------------------------------
11
11
12−using (xs : Vect k a)
13− ||| A proof that some element is found in a vector
12+||| A proof that some element is found in a vector
14− data Elem : a -> Vect k a -> Type where
13+data Elem : a -> Vect k a -> Type where
15− Here : Elem x (x::xs)
14+ Here : Elem x (x::xs)
16− There : Elem x xs -> Elem x (y::xs)
15+ There : Elem x xs -> Elem x (y::xs)
17
16
18||| Nothing can be in an empty Vect
17||| Nothing can be in an empty Vect
19noEmptyElem : {x : a} -> Elem x [] -> _|_
18noEmptyElem : {x : a} -> Elem x [] -> _|_
libs/neweffects/Effects.idr+8−9
@@ -55,15 +55,14 @@ syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
55syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
55syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
56
56
57-- --------------------------------------- [ Properties and Proof Construction ]
57-- --------------------------------------- [ Properties and Proof Construction ]
58−using (xs : List a, ys : List a)
59− data SubList : List a -> List a -> Type where
58+data SubList : List a -> List a -> Type where
60− SubNil : SubList {a} [] []
59+ SubNil : SubList [] []
61− Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)
60+ Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)
62− Drop : SubList xs ys -> SubList xs (x :: ys)
61+ Drop : SubList xs ys -> SubList xs (x :: ys)
63−
62+
64− subListId : SubList xs xs
63+subListId : SubList xs xs
65− subListId {xs = Nil} = SubNil
64+subListId {xs = Nil} = SubNil
66− subListId {xs = x :: xs} = Keep subListId
65+subListId {xs = x :: xs} = Keep subListId
67
66
68namespace Env
67namespace Env
69 data Env : (m : Type -> Type) -> List EFFECT -> Type where
68 data Env : (m : Type -> Type) -> List EFFECT -> Type where