git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4156 from msmorgan/fix-fixities
2eec999Ahmad Salim Al-Sibahi
libs/contrib/Interfaces/Correlative.idr+3−3
compare with master
unifiedsplit
@@ -5,7 +5,7 @@ import Data.Vect
5%access public export
5%access public export
6%default total
6%default total
7
7
8−infixl 2 </>
8+infixl 3 </>
9
9
10||| A Correlative functor is a functor where, given `(xs, ys : Correlative f)`,
10||| A Correlative functor is a functor where, given `(xs, ys : Correlative f)`,
11||| certain elements from xs and ys can be paired with one another due to some
11||| certain elements from xs and ys can be paired with one another due to some
@@ -13,11 +13,11 @@ infixl 2 </>
13interface Functor f => Correlative (f : Type -> Type) where
13interface Functor f => Correlative (f : Type -> Type) where
14 (</>) : f (a -> b) -> f a -> f b
14 (</>) : f (a -> b) -> f a -> f b
15
15
16−infixl 2 </
16+infixl 3 </
17(</) : Correlative f => f a -> f b -> f a
17(</) : Correlative f => f a -> f b -> f a
18x </ y = map const x </> y
18x </ y = map const x </> y
19
19
20−infixl 2 />
20+infixl 3 />
21(/>) : Correlative f => f a -> f b -> f b
21(/>) : Correlative f => f a -> f b -> f b
22x /> y = map (const id) x </> y
22x /> y = map (const id) x </> y
23
23
libs/effects/Effects.idr−2
@@ -303,8 +303,6 @@ staticEff = id
303toEff : .(xs' : List EFFECT) -> EffM m a xs (\v => xs') -> EffM m a xs (\v => xs')
303toEff : .(xs' : List EFFECT) -> EffM m a xs (\v => xs') -> EffM m a xs (\v => xs')
304toEff xs' = id
304toEff xs' = id
305
305
306−infixl 2 <*>
307−
308pure : a -> EffM m a xs (\v => xs)
306pure : a -> EffM m a xs (\v => xs)
309pure = Value
307pure = Value
310
308
libs/prelude/Prelude/Applicative.idr+4−4
@@ -12,17 +12,17 @@ import Prelude.Functor
12
12
13---- Applicative functors/Idioms
13---- Applicative functors/Idioms
14
14
15−infixl 2 <*>
15+infixl 3 <*>
16
16
17interface Functor f => Applicative (f : Type -> Type) where
17interface Functor f => Applicative (f : Type -> Type) where
18 pure : a -> f a
18 pure : a -> f a
19 (<*>) : f (a -> b) -> f a -> f b
19 (<*>) : f (a -> b) -> f a -> f b
20
20
21−infixl 2 <*
21+infixl 3 <*
22(<*) : Applicative f => f a -> f b -> f a
22(<*) : Applicative f => f a -> f b -> f a
23a <* b = map const a <*> b
23a <* b = map const a <*> b
24
24
25−infixl 2 *>
25+infixl 3 *>
26(*>) : Applicative f => f a -> f b -> f b
26(*>) : Applicative f => f a -> f b -> f b
27a *> b = map (const id) a <*> b
27a *> b = map (const id) a <*> b
28
28
@@ -38,7 +38,7 @@ liftA2 f a b = (map f a) <*> b
38liftA3 : Applicative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d
38liftA3 : Applicative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d
39liftA3 f a b c = (map f a) <*> b <*> c
39liftA3 f a b c = (map f a) <*> b <*> c
40
40
41−infixr 3 <|>
41+infixr 2 <|>
42interface Applicative f => Alternative (f : Type -> Type) where
42interface Applicative f => Alternative (f : Type -> Type) where
43 empty : f a
43 empty : f a
44 (<|>) : f a -> f a -> f a
44 (<|>) : f a -> f a -> f a
libs/prelude/Prelude/Basics.idr+1−2
@@ -29,7 +29,7 @@ fst (x, y) = x
29snd : (a, b) -> b
29snd : (a, b) -> b
30snd (x, y) = y
30snd (x, y) = y
31
31
32−infixl 9 .
32+infixr 9 .
33
33
34||| Function composition
34||| Function composition
35(.) : (b -> c) -> (a -> b) -> a -> c
35(.) : (b -> c) -> (a -> b) -> a -> c
@@ -58,4 +58,3 @@ data Dec : Type -> Type where
58 ||| The case where the property holding would be a contradiction
58 ||| The case where the property holding would be a contradiction
59 ||| @ contra a demonstration that prop would be a contradiction
59 ||| @ contra a demonstration that prop would be a contradiction
60 No : (contra : prop -> Void) -> Dec prop
60 No : (contra : prop -> Void) -> Dec prop
61−
libs/prelude/Prelude/Functor.idr+3−3
@@ -6,15 +6,15 @@ import Prelude.Basics
6%access public export
6%access public export
7
7
8||| Functors allow a uniform action over a parameterised type.
8||| Functors allow a uniform action over a parameterised type.
9−||| @ f a parameterised type
9+||| @ f a parameterised type
10interface Functor (f : Type -> Type) where
10interface Functor (f : Type -> Type) where
11− ||| Apply a function across everything of type 'a' in a
11+ ||| Apply a function across everything of type 'a' in a
12 ||| parameterised type
12 ||| parameterised type
13 ||| @ f the parameterised type
13 ||| @ f the parameterised type
14 ||| @ func the function to apply
14 ||| @ func the function to apply
15 map : (func : a -> b) -> f a -> f b
15 map : (func : a -> b) -> f a -> f b
16
16
17−infixl 4 <$>
17+infixr 4 <$>
18
18
19||| An infix alias for `map`, applying a function across everything of
19||| An infix alias for `map`, applying a function across everything of
20||| type 'a' in a parameterised type
20||| type 'a' in a parameterised type
libs/prelude/Prelude/Monad.idr+1−1
@@ -11,7 +11,7 @@ import IO
11
11
12%access public export
12%access public export
13
13
14−infixl 5 >>=
14+infixl 1 >>=
15
15
16interface Applicative m => Monad (m : Type -> Type) where
16interface Applicative m => Monad (m : Type -> Type) where
17 ||| Also called `bind`.
17 ||| Also called `bind`.