git.iko.soy/Idris-dev
on master help sign in
Change precedence of ++ to be higher than ::
2037fe8Edwin Brady
lib/prelude/list.idr+1−1
compare with master
unifiedsplit
@@ -8,7 +8,7 @@ import prelude.nat
8
8
9%access public
9%access public
10
10
11−infixr 10 ::
11+infixr 7 ::
12
12
13data List a
13data List a
14 = Nil
14 = Nil
lib/prelude/vect.idr+2−1
@@ -6,7 +6,7 @@ import prelude.nat
6
6
7%access public
7%access public
8
8
9−infixr 10 ::
9+infixr 7 ::
10
10
11data Vect : Set -> Nat -> Set where
11data Vect : Set -> Nat -> Set where
12 Nil : Vect a O
12 Nil : Vect a O
@@ -67,6 +67,7 @@ fromList (x::xs) = x :: fromList xs
67-- Building bigger vectors
67-- Building bigger vectors
68--------------------------------------------------------------------------------
68--------------------------------------------------------------------------------
69
69
70+total
70(++) : Vect a m -> Vect a n -> Vect a (m + n)
71(++) : Vect a m -> Vect a n -> Vect a (m + n)
71(++) [] ys = ys
72(++) [] ys = ys
72(++) (x::xs) ys = x :: xs ++ ys
73(++) (x::xs) ys = x :: xs ++ ys