Change precedence of ++ to be higher than ::
commit2037fe81c106d5abb34b32a54da05d7961995c95
authorEdwin Brady <eb@cs.st-andrews.ac.uk>
dateWed 14 Mar 2012, 09:45 (15 years ago)
parent7b10040
lib/prelude/list.idr+1−1
@@ -8,7 +8,7 @@ import prelude.nat
88
99%access public
1010
11−infixr 10 ::
11+infixr 7 ::
1212
1313data List a
1414 = Nil
lib/prelude/vect.idr+2−1
@@ -6,7 +6,7 @@ import prelude.nat
66
77%access public
88
9−infixr 10 ::
9+infixr 7 ::
1010
1111data Vect : Set -> Nat -> Set where
1212 Nil : Vect a O
@@ -67,6 +67,7 @@ fromList (x::xs) = x :: fromList xs
6767-- Building bigger vectors
6868--------------------------------------------------------------------------------
6969
70+total
7071(++) : Vect a m -> Vect a n -> Vect a (m + n)
7172(++) [] ys = ys
7273(++) (x::xs) ys = x :: xs ++ ys