git.iko.soy/Idris-dev
on master help sign in
Prelude: rework operator fixity
commitba92987fdd4fc6ef2e4d7ad09bc87be84265eeac authorMichael Morgan <morgan.michael@me.com> dateTue 10 Oct 2017, 15:16 (9 years ago) parent7081ff0
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
@@ -15,6 +15,7 @@
1515+ Added `Data.IORef`, for working with mutable references in `IO` and `JS_IO`.
1616+ Added `discriminate` and `construct` tactics to Pruviloj.
1717+ Added `IsSucc` type to `Prelude`, which proves that a `Nat` is a successor.
18++ Reworked operator fixity for `&&` and `||`, as well as the comparison operators: `==`, `/=`, `<`, `<=`, `>`, and `>=`.
1819
1920## Tool Updates
2021+ 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