git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4113 from msmorgan/boolean-op-fixity

Prelude: rework operator fixity for comparison and boolean operators

commit22d95eba0f5e4f55d542f9e07915ed3ebbed0dd4 authorAhmad Salim Al-Sibahi <asal@itu.dk> dateTue 24 Oct 2017, 15:35 (9 years ago) parent852be39eed742e
4 files changed+10−9
compare with master
unifiedsplit
CHANGELOG.md+1 libs/prelude/Prelude.idr+2−2 libs/prelude/Prelude/Bool.idr+3−2 libs/prelude/Prelude/Interfaces.idr+4−5
CHANGELOG.md+1
@@ -24,6 +24,7 @@
2424+ Added `IsSucc` type to `Prelude`, which proves that a `Nat` is a successor.
2525+ Added `Data.IOArray`, containing primitives for mutable arrays.
2626+ The operator `<|>` is now right-associative (it retains the same precedence).
27++ Reworked operator fixity for `&&` and `||`, as well as the comparison operators: `==`, `/=`, `<`, `<=`, `>`, and `>=`.
2728
2829## Tool Updates
2930+ 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
212212 go : Integer -> Integer -> List Integer
213213 go n m = go' n (natRange (S (cast {to = Nat} (m - n))))
214214 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 []
216216 else go (natRange (S (divNatNZ (fromInteger (abs (m - n))) (S (fromInteger ((abs (next - n)) - 1))) SIsNotZ)))
217217 where go : List Nat -> List Integer
218218 go [] = []
@@ -234,7 +234,7 @@ Enum Int where
234234 enumFromThen n inc = countFrom n (inc - n)
235235
236236 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 []
238238 else go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs (next - n)) - 1))) SIsNotZ)))
239239 where go : List Nat -> List Int
240240 go [] = []
libs/prelude/Prelude/Bool.idr+3−2
@@ -18,7 +18,8 @@ ifThenElse True t e = t
1818ifThenElse False t e = e
1919
2020-- Boolean Operator Precedence
21−infixl 4 &&, ||
21+infixr 4 ||
22+infixr 5 &&
2223
2324||| Boolean OR only evaluates the second argument if the first is `False`.
2425(||) : Bool -> Lazy Bool -> Bool
@@ -43,4 +44,4 @@ Uninhabited (True = False) where
4344 uninhabited Refl impossible
4445
4546Uninhabited (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
77%access public export
88
99-- Numerical Operator Precedence
10−infixl 5 ==, /=
11−infixl 6 <, <=, >, >=
12−infixl 7 <<, >>
13−infixl 8 +,-
14−infixl 9 *,/
10+infix 6 ==, /=, <, <=, >, >=
11+infixl 7 <<, >> -- unused
12+infixl 8 +, -
13+infixl 9 *, /
1514
1615-- ------------------------------------------------------------- [ Boolean Ops ]
1716intToBool : Int -> Bool