{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Data.Integer.Base where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Data.Empty
import qualified MAlonzo.Code.Data.Nat.Base
import qualified MAlonzo.Code.Data.Sign.Base

-- Data.Integer.Base.0ℤ
d_0ℤ_12 :: Integer
d_0ℤ_12 :: Integer
d_0ℤ_12 = Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
-- Data.Integer.Base.-1ℤ
d_'45'1ℤ_14 :: Integer
d_'45'1ℤ_14 :: Integer
d_'45'1ℤ_14 = Integer -> Integer
forall a b. a -> b
coe (-Integer
1 :: Integer)
-- Data.Integer.Base.1ℤ
d_1ℤ_16 :: Integer
d_1ℤ_16 :: Integer
d_1ℤ_16 = Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)
-- Data.Integer.Base.∣_∣
d_'8739'_'8739'_18 :: Integer -> Integer
d_'8739'_'8739'_18 :: Integer -> Integer
d_'8739'_'8739'_18 Integer
v0
  = case Integer -> Any
forall a b. a -> b
coe Integer
v0 of
      Any
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) -> Integer -> Integer
forall a b. a -> b
coe Integer
v0
      Any
_ -> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
subInt (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)
-- Data.Integer.Base.sign
d_sign_24 :: Integer -> MAlonzo.Code.Data.Sign.Base.T_Sign_6
d_sign_24 :: Integer -> T_Sign_6
d_sign_24 Integer
v0
  = case Integer -> Any
forall a b. a -> b
coe Integer
v0 of
      Any
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) ->
          T_Sign_6 -> T_Sign_6
forall a b. a -> b
coe T_Sign_6
MAlonzo.Code.Data.Sign.Base.C_'43'_10
      Any
_ -> T_Sign_6 -> T_Sign_6
forall a b. a -> b
coe T_Sign_6
MAlonzo.Code.Data.Sign.Base.C_'45'_8
-- Data.Integer.Base._≤_
d__'8804'__26 :: p -> p -> ()
d__'8804'__26 p
a0 p
a1 = ()
data T__'8804'__26
  = C_'45''8804''45'_34 MAlonzo.Code.Data.Nat.Base.T__'8804'__18 |
    C_'45''8804''43'_40 |
    C_'43''8804''43'_48 MAlonzo.Code.Data.Nat.Base.T__'8804'__18
-- Data.Integer.Base._<_
d__'60'__50 :: p -> p -> ()
d__'60'__50 p
a0 p
a1 = ()
data T__'60'__50
  = C_'45''60''45'_58 MAlonzo.Code.Data.Nat.Base.T__'8804'__18 |
    C_'45''60''43'_64 |
    C_'43''60''43'_72 MAlonzo.Code.Data.Nat.Base.T__'8804'__18
-- Data.Integer.Base._≥_
d__'8805'__74 :: Integer -> Integer -> ()
d__'8805'__74 :: Integer -> Integer -> ()
d__'8805'__74 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Integer.Base._>_
d__'62'__80 :: Integer -> Integer -> ()
d__'62'__80 :: Integer -> Integer -> ()
d__'62'__80 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Integer.Base._≰_
d__'8816'__86 :: Integer -> Integer -> ()
d__'8816'__86 :: Integer -> Integer -> ()
d__'8816'__86 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Integer.Base._≱_
d__'8817'__92 :: Integer -> Integer -> ()
d__'8817'__92 :: Integer -> Integer -> ()
d__'8817'__92 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Integer.Base._≮_
d__'8814'__98 :: Integer -> Integer -> ()
d__'8814'__98 :: Integer -> Integer -> ()
d__'8814'__98 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Integer.Base._≯_
d__'8815'__104 :: Integer -> Integer -> ()
d__'8815'__104 :: Integer -> Integer -> ()
d__'8815'__104 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Integer.Base._≤ᵇ_
d__'8804''7495'__110 :: Integer -> Integer -> Bool
d__'8804''7495'__110 :: Integer -> Integer -> Bool
d__'8804''7495'__110 Integer
v0 Integer
v1
  = case Integer -> Any
forall a b. a -> b
coe Integer
v0 of
      Any
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) ->
          case Integer -> Any
forall a b. a -> b
coe Integer
v1 of
            Any
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) ->
                (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe
                  Integer -> Integer -> Bool
MAlonzo.Code.Data.Nat.Base.d__'8804''7495'__10 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
            Any
_ -> Bool -> Bool
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
      Any
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe (-Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0) in
           Any -> Bool
forall a b. a -> b
coe
             (case Integer -> Any
forall a b. a -> b
coe Integer
v1 of
                Any
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) ->
                    Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10
                Any
_ -> let v3 :: Integer
v3 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe (-Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1) in
                     Any -> Any
forall a b. a -> b
coe
                       ((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
                          Integer -> Integer -> Bool
MAlonzo.Code.Data.Nat.Base.d__'8804''7495'__10 (Integer -> Any
forall a b. a -> b
coe Integer
v3) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
-- Data.Integer.Base.NonZero
d_NonZero_128 :: Integer -> ()
d_NonZero_128 :: Integer -> ()
d_NonZero_128 = Integer -> ()
forall a. a
erased
-- Data.Integer.Base.Positive
d_Positive_132 :: Integer -> ()
d_Positive_132 :: Integer -> ()
d_Positive_132 = Integer -> ()
forall a. a
erased
-- Data.Integer.Base.Negative
d_Negative_138 :: Integer -> ()
d_Negative_138 :: Integer -> ()
d_Negative_138 = Integer -> ()
forall a. a
erased
-- Data.Integer.Base.NonPositive
d_NonPositive_144 :: Integer -> ()
d_NonPositive_144 :: Integer -> ()
d_NonPositive_144 = Integer -> ()
forall a. a
erased
-- Data.Integer.Base.NonNegative
d_NonNegative_150 :: Integer -> ()
d_NonNegative_150 :: Integer -> ()
d_NonNegative_150 = Integer -> ()
forall a. a
erased
-- Data.Integer.Base.≢-nonZero
d_'8802''45'nonZero_158 ::
  Integer ->
  (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
   MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  AgdaAny
d_'8802''45'nonZero_158 :: Integer -> (T__'8801'__12 -> T_'8869'_4) -> Any
d_'8802''45'nonZero_158 Integer
v0 T__'8801'__12 -> T_'8869'_4
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> (T__'8801'__12 -> T_'8869'_4) -> Any -> Any
forall a b. a -> b
coe T__'8801'__12 -> T_'8869'_4
v1 Any
forall a. a
erased
      Integer
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
          () -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8
      Integer
_ -> () -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8
-- Data.Integer.Base.>-nonZero
d_'62''45'nonZero_168 :: Integer -> T__'60'__50 -> AgdaAny
d_'62''45'nonZero_168 :: Integer -> T__'60'__50 -> Any
d_'62''45'nonZero_168 ~Integer
v0 T__'60'__50
v1 = T__'60'__50 -> Any
du_'62''45'nonZero_168 T__'60'__50
v1
du_'62''45'nonZero_168 :: T__'60'__50 -> AgdaAny
du_'62''45'nonZero_168 :: T__'60'__50 -> Any
du_'62''45'nonZero_168 T__'60'__50
v0
  = case T__'60'__50 -> T__'60'__50
forall a b. a -> b
coe T__'60'__50
v0 of
      C_'43''60''43'_72 T__'8804'__18
v3
        -> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> Any
forall a b. a -> b -> b
seq (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v3) (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
      T__'60'__50
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Integer.Base.<-nonZero
d_'60''45'nonZero_174 :: Integer -> T__'60'__50 -> AgdaAny
d_'60''45'nonZero_174 :: Integer -> T__'60'__50 -> Any
d_'60''45'nonZero_174 ~Integer
v0 T__'60'__50
v1 = T__'60'__50 -> Any
du_'60''45'nonZero_174 T__'60'__50
v1
du_'60''45'nonZero_174 :: T__'60'__50 -> AgdaAny
du_'60''45'nonZero_174 :: T__'60'__50 -> Any
du_'60''45'nonZero_174 T__'60'__50
v0
  = (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> Any
forall a b. a -> b -> b
seq (T__'60'__50 -> Any
forall a b. a -> b
coe T__'60'__50
v0) (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
-- Data.Integer.Base.positive
d_positive_178 :: Integer -> T__'60'__50 -> AgdaAny
d_positive_178 :: Integer -> T__'60'__50 -> Any
d_positive_178 ~Integer
v0 T__'60'__50
v1 = T__'60'__50 -> Any
du_positive_178 T__'60'__50
v1
du_positive_178 :: T__'60'__50 -> AgdaAny
du_positive_178 :: T__'60'__50 -> Any
du_positive_178 T__'60'__50
v0
  = case T__'60'__50 -> T__'60'__50
forall a b. a -> b
coe T__'60'__50
v0 of
      C_'43''60''43'_72 T__'8804'__18
v3
        -> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> Any
forall a b. a -> b -> b
seq (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v3) (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
      T__'60'__50
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Integer.Base.negative
d_negative_184 :: Integer -> T__'60'__50 -> AgdaAny
d_negative_184 :: Integer -> T__'60'__50 -> Any
d_negative_184 ~Integer
v0 T__'60'__50
v1 = T__'60'__50 -> Any
du_negative_184 T__'60'__50
v1
du_negative_184 :: T__'60'__50 -> AgdaAny
du_negative_184 :: T__'60'__50 -> Any
du_negative_184 T__'60'__50
v0
  = (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> Any
forall a b. a -> b -> b
seq (T__'60'__50 -> Any
forall a b. a -> b
coe T__'60'__50
v0) (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
-- Data.Integer.Base.nonPositive
d_nonPositive_188 :: Integer -> T__'8804'__26 -> AgdaAny
d_nonPositive_188 :: Integer -> T__'8804'__26 -> Any
d_nonPositive_188 ~Integer
v0 T__'8804'__26
v1 = T__'8804'__26 -> Any
du_nonPositive_188 T__'8804'__26
v1
du_nonPositive_188 :: T__'8804'__26 -> AgdaAny
du_nonPositive_188 :: T__'8804'__26 -> Any
du_nonPositive_188 T__'8804'__26
v0
  = case T__'8804'__26 -> T__'8804'__26
forall a b. a -> b
coe T__'8804'__26
v0 of
      T__'8804'__26
C_'45''8804''43'_40 -> () -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8
      C_'43''8804''43'_48 T__'8804'__18
v3
        -> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> Any
forall a b. a -> b -> b
seq (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v3) (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
      T__'8804'__26
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Integer.Base.nonNegative
d_nonNegative_192 :: Integer -> T__'8804'__26 -> AgdaAny
d_nonNegative_192 :: Integer -> T__'8804'__26 -> Any
d_nonNegative_192 Integer
v0 ~T__'8804'__26
v1 = Integer -> Any
du_nonNegative_192 Integer
v0
du_nonNegative_192 :: Integer -> AgdaAny
du_nonNegative_192 :: Integer -> Any
du_nonNegative_192 Integer
v0
  = (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> Any
forall a b. a -> b -> b
seq (Integer -> Any
forall a b. a -> b
coe Integer
v0) (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
-- Data.Integer.Base._◃_
d__'9667'__196 ::
  MAlonzo.Code.Data.Sign.Base.T_Sign_6 -> Integer -> Integer
d__'9667'__196 :: T_Sign_6 -> Integer -> Integer
d__'9667'__196 T_Sign_6
v0 Integer
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
      Integer
0 -> Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
      Integer
_ -> case T_Sign_6 -> T_Sign_6
forall a b. a -> b
coe T_Sign_6
v0 of
             T_Sign_6
MAlonzo.Code.Data.Sign.Base.C_'45'_8
               -> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
subInt (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
             T_Sign_6
MAlonzo.Code.Data.Sign.Base.C_'43'_10 -> Integer -> Integer
forall a b. a -> b
coe Integer
v1
             T_Sign_6
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Integer.Base.SignAbs
d_SignAbs_202 :: p -> ()
d_SignAbs_202 p
a0 = ()
data T_SignAbs_202
  = C__'9666'__208 MAlonzo.Code.Data.Sign.Base.T_Sign_6 Integer
-- Data.Integer.Base.signAbs
d_signAbs_212 :: Integer -> T_SignAbs_202
d_signAbs_212 :: Integer -> T_SignAbs_202
d_signAbs_212 Integer
v0
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> (T_Sign_6 -> Integer -> T_SignAbs_202)
-> Any -> Any -> T_SignAbs_202
forall a b. a -> b
coe
             T_Sign_6 -> Integer -> T_SignAbs_202
C__'9666'__208 (T_Sign_6 -> Any
forall a b. a -> b
coe T_Sign_6
MAlonzo.Code.Data.Sign.Base.C_'43'_10)
             (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
      Integer
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
          (T_Sign_6 -> Integer -> T_SignAbs_202)
-> Any -> Any -> T_SignAbs_202
forall a b. a -> b
coe
            T_Sign_6 -> Integer -> T_SignAbs_202
C__'9666'__208 (T_Sign_6 -> Any
forall a b. a -> b
coe T_Sign_6
MAlonzo.Code.Data.Sign.Base.C_'43'_10) (Integer -> Any
forall a b. a -> b
coe Integer
v0)
      Integer
_ -> (T_Sign_6 -> Integer -> T_SignAbs_202)
-> Any -> Any -> T_SignAbs_202
forall a b. a -> b
coe
             T_Sign_6 -> Integer -> T_SignAbs_202
C__'9666'__208 (T_Sign_6 -> Any
forall a b. a -> b
coe T_Sign_6
MAlonzo.Code.Data.Sign.Base.C_'45'_8)
             ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
subInt (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
-- Data.Integer.Base.-_
d_'45'__218 :: Integer -> Integer
d_'45'__218 :: Integer -> Integer
d_'45'__218 Integer
v0 = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
subInt (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)
-- Data.Integer.Base._⊖_
d__'8854'__224 :: Integer -> Integer -> Integer
d__'8854'__224 :: Integer -> Integer -> Integer
d__'8854'__224 Integer
v0 Integer
v1
  = let v2 :: Bool
v2 = Integer -> Integer -> Bool
ltInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v1) in
    Any -> Integer
forall a b. a -> b
coe
      (if Bool -> Bool
forall a b. a -> b
coe Bool
v2
         then (Integer -> Integer) -> Any -> Any
forall a b. a -> b
coe Integer -> Integer
d_'45'__218 ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
subInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
         else (Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
subInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
-- Data.Integer.Base._+_
d__'43'__242 :: Integer -> Integer -> Integer
d__'43'__242 :: Integer -> Integer -> Integer
d__'43'__242 Integer
v0 Integer
v1
  = case Integer -> Any
forall a b. a -> b
coe Integer
v0 of
      Any
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) ->
          case Integer -> Any
forall a b. a -> b
coe Integer
v1 of
            Any
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) ->
                (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
            Any
_ -> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
                   Integer -> Integer -> Integer
d__'8854'__224 (Integer -> Any
forall a b. a -> b
coe Integer
v0) ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
subInt (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
      Any
_ -> case Integer -> Any
forall a b. a -> b
coe Integer
v1 of
             Any
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) ->
                 (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
                   Integer -> Integer -> Integer
d__'8854'__224 (Integer -> Any
forall a b. a -> b
coe Integer
v1) ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
subInt (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
             Any
_ -> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
-- Data.Integer.Base._-_
d__'45'__260 :: Integer -> Integer -> Integer
d__'45'__260 :: Integer -> Integer -> Integer
d__'45'__260 Integer
v0 Integer
v1
  = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
d__'43'__242 (Integer -> Any
forall a b. a -> b
coe Integer
v0) ((Integer -> Integer) -> Any -> Any
forall a b. a -> b
coe Integer -> Integer
d_'45'__218 (Integer -> Any
forall a b. a -> b
coe Integer
v1))
-- Data.Integer.Base.suc
d_suc_266 :: Integer -> Integer
d_suc_266 :: Integer -> Integer
d_suc_266 Integer
v0 = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
d__'43'__242 (Integer -> Any
forall a b. a -> b
coe Integer
d_1ℤ_16) (Integer -> Any
forall a b. a -> b
coe Integer
v0)
-- Data.Integer.Base.pred
d_pred_270 :: Integer -> Integer
d_pred_270 :: Integer -> Integer
d_pred_270 Integer
v0 = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
d__'43'__242 (Integer -> Any
forall a b. a -> b
coe Integer
d_'45'1ℤ_14) (Integer -> Any
forall a b. a -> b
coe Integer
v0)
-- Data.Integer.Base._*_
d__'42'__274 :: Integer -> Integer -> Integer
d__'42'__274 :: Integer -> Integer -> Integer
d__'42'__274 Integer
v0 Integer
v1
  = (T_Sign_6 -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
      T_Sign_6 -> Integer -> Integer
d__'9667'__196
      ((T_Sign_6 -> T_Sign_6 -> T_Sign_6) -> Any -> Any -> Any
forall a b. a -> b
coe
         T_Sign_6 -> T_Sign_6 -> T_Sign_6
MAlonzo.Code.Data.Sign.Base.d__'42'__14 ((Integer -> T_Sign_6) -> Any -> Any
forall a b. a -> b
coe Integer -> T_Sign_6
d_sign_24 (Integer -> Any
forall a b. a -> b
coe Integer
v0))
         ((Integer -> T_Sign_6) -> Any -> Any
forall a b. a -> b
coe Integer -> T_Sign_6
d_sign_24 (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
      ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
         Integer -> Integer -> Integer
mulInt ((Integer -> Integer) -> Any -> Any
forall a b. a -> b
coe Integer -> Integer
d_'8739'_'8739'_18 (Integer -> Any
forall a b. a -> b
coe Integer
v0))
         ((Integer -> Integer) -> Any -> Any
forall a b. a -> b
coe Integer -> Integer
d_'8739'_'8739'_18 (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
-- Data.Integer.Base._⊔_
d__'8852'__280 :: Integer -> Integer -> Integer
d__'8852'__280 :: Integer -> Integer -> Integer
d__'8852'__280 Integer
v0 Integer
v1
  = case Integer -> Any
forall a b. a -> b
coe Integer
v0 of
      Any
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) ->
          case Integer -> Any
forall a b. a -> b
coe Integer
v1 of
            Any
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) ->
                (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d__'8852'__106 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
            Any
_ -> Integer -> Integer
forall a b. a -> b
coe Integer
v0
      Any
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe (-Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0) in
           Any -> Integer
forall a b. a -> b
coe
             (case Integer -> Any
forall a b. a -> b
coe Integer
v1 of
                Any
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) -> Integer -> Any
forall a b. a -> b
coe Integer
v1
                Any
_ -> let v3 :: Integer
v3 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe (-Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1) in
                     Any -> Any
forall a b. a -> b
coe
                       ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                          Integer -> Integer -> Integer
subInt (Integer -> Any
forall a b. a -> b
coe (-Integer
1 :: Integer))
                          ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d__'8851'__116 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3))))
-- Data.Integer.Base._⊓_
d__'8851'__298 :: Integer -> Integer -> Integer
d__'8851'__298 :: Integer -> Integer -> Integer
d__'8851'__298 Integer
v0 Integer
v1
  = case Integer -> Any
forall a b. a -> b
coe Integer
v0 of
      Any
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) ->
          case Integer -> Any
forall a b. a -> b
coe Integer
v1 of
            Any
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) ->
                (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d__'8851'__116 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
            Any
_ -> Integer -> Integer
forall a b. a -> b
coe Integer
v1
      Any
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe (-Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0) in
           Any -> Integer
forall a b. a -> b
coe
             (case Integer -> Any
forall a b. a -> b
coe Integer
v1 of
                Any
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) -> Integer -> Any
forall a b. a -> b
coe Integer
v0
                Any
_ -> let v3 :: Integer
v3 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe (-Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1) in
                     Any -> Any
forall a b. a -> b
coe
                       ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                          Integer -> Integer -> Integer
subInt (Integer -> Any
forall a b. a -> b
coe (-Integer
1 :: Integer))
                          ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d__'8852'__106 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3))))
-- Data.Integer.Base._<′_
d__'60''8242'__316 :: Integer -> Integer -> ()
d__'60''8242'__316 :: Integer -> Integer -> ()
d__'60''8242'__316 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Integer.Base._>′_
d__'62''8242'__322 :: Integer -> Integer -> ()
d__'62''8242'__322 :: Integer -> Integer -> ()
d__'62''8242'__322 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Integer.Base._≮′_
d__'8814''8242'__328 :: Integer -> Integer -> ()
d__'8814''8242'__328 :: Integer -> Integer -> ()
d__'8814''8242'__328 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Integer.Base._≯′_
d__'8815''8242'__334 :: Integer -> Integer -> ()
d__'8815''8242'__334 :: Integer -> Integer -> ()
d__'8815''8242'__334 = Integer -> Integer -> ()
forall a. a
erased