git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4113 from msmorgan/boolean-op-fixity
22d95ebAhmad Salim Al-Sibahi
CHANGELOG.md+1
compare with master
unifiedsplit
@@ -24,6 +24,7 @@
24+ Added `IsSucc` type to `Prelude`, which proves that a `Nat` is a successor.
24+ Added `IsSucc` type to `Prelude`, which proves that a `Nat` is a successor.
25+ Added `Data.IOArray`, containing primitives for mutable arrays.
25+ Added `Data.IOArray`, containing primitives for mutable arrays.
26+ The operator `<|>` is now right-associative (it retains the same precedence).
26+ The operator `<|>` is now right-associative (it retains the same precedence).
27++ Reworked operator fixity for `&&` and `||`, as well as the comparison operators: `==`, `/=`, `<`, `<=`, `>`, and `>=`.
27
28
28## Tool Updates
29## Tool Updates
29+ Private functions are no longer visible in the REPL except for modules
30+ Private functions are no longer visible in the REPL except for modules
libs/prelude/Prelude.idr+2−2
@@ -212,7 +212,7 @@ Enum Integer where
212 go : Integer -> Integer -> List Integer
212 go : Integer -> Integer -> List Integer
213 go n m = go' n (natRange (S (cast {to = Nat} (m - n))))
213 go n m = go' n (natRange (S (cast {to = Nat} (m - n))))
214 enumFromThenTo n next m = if n == m then [n]
214 enumFromThenTo n next m = if n == m then [n]
215− else if next - n == 0 || next - n < 0 /= m - n < 0 then []
215+ else if next - n == 0 || (next - n < 0) /= (m - n < 0) then []
216 else go (natRange (S (divNatNZ (fromInteger (abs (m - n))) (S (fromInteger ((abs (next - n)) - 1))) SIsNotZ)))
216 else go (natRange (S (divNatNZ (fromInteger (abs (m - n))) (S (fromInteger ((abs (next - n)) - 1))) SIsNotZ)))
217 where go : List Nat -> List Integer
217 where go : List Nat -> List Integer
218 go [] = []
218 go [] = []
@@ -234,7 +234,7 @@ Enum Int where
234 enumFromThen n inc = countFrom n (inc - n)
234 enumFromThen n inc = countFrom n (inc - n)
235
235
236 enumFromThenTo n next m = if n == m then [n]
236 enumFromThenTo n next m = if n == m then [n]
237− else if next - n == 0 || next - n < 0 /= m - n < 0 then []
237+ else if next - n == 0 || (next - n < 0) /= (m - n < 0) then []
238 else go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs (next - n)) - 1))) SIsNotZ)))
238 else go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs (next - n)) - 1))) SIsNotZ)))
239 where go : List Nat -> List Int
239 where go : List Nat -> List Int
240 go [] = []
240 go [] = []
libs/prelude/Prelude/Bool.idr+3−2
@@ -18,7 +18,8 @@ ifThenElse True t e = t
18ifThenElse False t e = e
18ifThenElse False t e = e
19
19
20-- Boolean Operator Precedence
20-- Boolean Operator Precedence
21−infixl 4 &&, ||
21+infixr 4 ||
22+infixr 5 &&
22
23
23||| Boolean OR only evaluates the second argument if the first is `False`.
24||| Boolean OR only evaluates the second argument if the first is `False`.
24(||) : Bool -> Lazy Bool -> Bool
25(||) : Bool -> Lazy Bool -> Bool
@@ -43,4 +44,4 @@ Uninhabited (True = False) where
43 uninhabited Refl impossible
44 uninhabited Refl impossible
44
45
45Uninhabited (False = True) where
46Uninhabited (False = True) where
46− uninhabited Refl impossible
47+ uninhabited Refl impossible
libs/prelude/Prelude/Interfaces.idr+4−5
@@ -7,11 +7,10 @@ import Prelude.Bool
7%access public export
7%access public export
8
8
9-- Numerical Operator Precedence
9-- Numerical Operator Precedence
10−infixl 5 ==, /=
10+infix 6 ==, /=, <, <=, >, >=
11−infixl 6 <, <=, >, >=
12−infixl 7 <<, >>
11+infixl 7 <<, >> -- unused
13−infixl 8 +,-
12+infixl 8 +, -
14−infixl 9 *,/
13+infixl 9 *, /
15
14
16-- ------------------------------------------------------------- [ Boolean Ops ]
15-- ------------------------------------------------------------- [ Boolean Ops ]
17intToBool : Int -> Bool
16intToBool : Int -> Bool