git.iko.soy/Idris-dev
on master help sign in
adjust fixities of common operators
commit8a34c865c2aa381356a2692d7db75b25676d011f authorMichael Morgan <morgan.michael@me.com> dateThu 26 Oct 2017, 22:13 (9 years ago) parentb83d4ba
6 files changed+12−15
compare with master
unifiedsplit
libs/contrib/Interfaces/Correlative.idr+3−3 libs/effects/Effects.idr−2 libs/prelude/Prelude/Applicative.idr+4−4 libs/prelude/Prelude/Basics.idr+1−2 libs/prelude/Prelude/Functor.idr+3−3 libs/prelude/Prelude/Monad.idr+1−1
libs/contrib/Interfaces/Correlative.idr+3−3
@@ -5,7 +5,7 @@ import Data.Vect
55%access public export
66%default total
77
8−infixl 2 </>
8+infixl 3 </>
99
1010||| A Correlative functor is a functor where, given `(xs, ys : Correlative f)`,
1111||| certain elements from xs and ys can be paired with one another due to some
@@ -13,11 +13,11 @@ infixl 2 </>
1313interface Functor f => Correlative (f : Type -> Type) where
1414 (</>) : f (a -> b) -> f a -> f b
1515
16−infixl 2 </
16+infixl 3 </
1717(</) : Correlative f => f a -> f b -> f a
1818x </ y = map const x </> y
1919
20−infixl 2 />
20+infixl 3 />
2121(/>) : Correlative f => f a -> f b -> f b
2222x /> y = map (const id) x </> y
2323
libs/effects/Effects.idr−2
@@ -303,8 +303,6 @@ staticEff = id
303303toEff : .(xs' : List EFFECT) -> EffM m a xs (\v => xs') -> EffM m a xs (\v => xs')
304304toEff xs' = id
305305
306−infixl 2 <*>
307−
308306pure : a -> EffM m a xs (\v => xs)
309307pure = Value
310308
libs/prelude/Prelude/Applicative.idr+4−4
@@ -12,17 +12,17 @@ import Prelude.Functor
1212
1313---- Applicative functors/Idioms
1414
15−infixl 2 <*>
15+infixl 3 <*>
1616
1717interface Functor f => Applicative (f : Type -> Type) where
1818 pure : a -> f a
1919 (<*>) : f (a -> b) -> f a -> f b
2020
21−infixl 2 <*
21+infixl 3 <*
2222(<*) : Applicative f => f a -> f b -> f a
2323a <* b = map const a <*> b
2424
25−infixl 2 *>
25+infixl 3 *>
2626(*>) : Applicative f => f a -> f b -> f b
2727a *> b = map (const id) a <*> b
2828
@@ -38,7 +38,7 @@ liftA2 f a b = (map f a) <*> b
3838liftA3 : Applicative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d
3939liftA3 f a b c = (map f a) <*> b <*> c
4040
41−infixr 3 <|>
41+infixr 2 <|>
4242interface Applicative f => Alternative (f : Type -> Type) where
4343 empty : f a
4444 (<|>) : f a -> f a -> f a
libs/prelude/Prelude/Basics.idr+1−2
@@ -29,7 +29,7 @@ fst (x, y) = x
2929snd : (a, b) -> b
3030snd (x, y) = y
3131
32−infixl 9 .
32+infixr 9 .
3333
3434||| Function composition
3535(.) : (b -> c) -> (a -> b) -> a -> c
@@ -58,4 +58,3 @@ data Dec : Type -> Type where
5858 ||| The case where the property holding would be a contradiction
5959 ||| @ contra a demonstration that prop would be a contradiction
6060 No : (contra : prop -> Void) -> Dec prop
61−
libs/prelude/Prelude/Functor.idr+3−3
@@ -6,15 +6,15 @@ import Prelude.Basics
66%access public export
77
88||| Functors allow a uniform action over a parameterised type.
9−||| @ f a parameterised type
9+||| @ f a parameterised type
1010interface 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
1212 ||| parameterised type
1313 ||| @ f the parameterised type
1414 ||| @ func the function to apply
1515 map : (func : a -> b) -> f a -> f b
1616
17−infixl 4 <$>
17+infixr 4 <$>
1818
1919||| An infix alias for `map`, applying a function across everything of
2020||| type 'a' in a parameterised type
libs/prelude/Prelude/Monad.idr+1−1
@@ -11,7 +11,7 @@ import IO
1111
1212%access public export
1313
14−infixl 5 >>=
14+infixl 1 >>=
1515
1616interface Applicative m => Monad (m : Type -> Type) where
1717 ||| Also called `bind`.