on master help sign in
change `<|>` operator to be right-associative
aa2b5b3Michael Morgan
CHANGELOG.md+1
@@ -15,6 +15,7 @@
15+ Added `Data.IORef`, for working with mutable references in `IO` and `JS_IO`.
15+ Added `Data.IORef`, for working with mutable references in `IO` and `JS_IO`.
16+ Added `discriminate` and `construct` tactics to Pruviloj.
16+ Added `discriminate` and `construct` tactics to Pruviloj.
17+ Added `IsSucc` type to `Prelude`, which proves that a `Nat` is a successor.
17+ Added `IsSucc` type to `Prelude`, which proves that a `Nat` is a successor.
18++ The operator `<|>` is now right-associative (it retains the same precedence).
18
19
19## Tool Updates
20## Tool Updates
20+ Private functions are no longer visible in the REPL except for modules
21+ Private functions are no longer visible in the REPL except for modules
libs/prelude/Prelude/Applicative.idr+1−1
@@ -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−infixl 3 <|>
41+infixr 3 <|>
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