Skip to content

Commit 7c1d356

Browse files
committed
Int cleanup
1 parent 6ab31b8 commit 7c1d356

File tree

1 file changed

+0
-7
lines changed

1 file changed

+0
-7
lines changed

lib/Haskell/Law/Ord/Int.agda

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -13,13 +13,6 @@ open import Haskell.Law.Eq
1313
open import Haskell.Law.Ord.Def
1414
open import Haskell.Law.Int
1515

16-
private
17-
18-
2⁶³ : Nat
19-
2⁶³ = 9223372036854775808
20-
21-
maxW : Word
22-
maxW = (n2w (monusNat 2⁶³ 1))
2316

2417
sign2neq : (a b : Int) isNegativeInt a ≡ True isNegativeInt b ≡ False ((a == b) ≡ False)
2518
sign2neq a@(int64 x) b@(int64 y) h₁ h₂ with a == b in h₃

0 commit comments

Comments
 (0)