{-# 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.Nat
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Algebra.Bundles.Raw
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.Nat.Base
import qualified MAlonzo.Code.Data.Sign.Base
import qualified MAlonzo.Code.Relation.Nullary.Negation.Core

-- 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'__22 |
    C_'45''8804''43'_40 |
    C_'43''8804''43'_48 MAlonzo.Code.Data.Nat.Base.T__'8804'__22
-- 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'__22 |
    C_'45''60''43'_64 |
    C_'43''60''43'_72 MAlonzo.Code.Data.Nat.Base.T__'8804'__22
-- 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'__14 (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'__14 (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_134 :: p -> ()
d_Positive_134 p
a0 = ()
newtype T_Positive_134 = C_constructor_142 AgdaAny
-- Data.Integer.Base.Positive.pos
d_pos_140 :: T_Positive_134 -> AgdaAny
d_pos_140 :: T_Positive_134 -> Any
d_pos_140 T_Positive_134
v0
  = case T_Positive_134 -> T_Positive_134
forall a b. a -> b
coe T_Positive_134
v0 of
      C_constructor_142 Any
v1 -> Any -> Any
forall a b. a -> b
coe Any
v1
      T_Positive_134
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Integer.Base.NonNegative
d_NonNegative_146 :: p -> ()
d_NonNegative_146 p
a0 = ()
newtype T_NonNegative_146 = C_constructor_154 AgdaAny
-- Data.Integer.Base.NonNegative.nonNeg
d_nonNeg_152 :: T_NonNegative_146 -> AgdaAny
d_nonNeg_152 :: T_NonNegative_146 -> Any
d_nonNeg_152 T_NonNegative_146
v0
  = case T_NonNegative_146 -> T_NonNegative_146
forall a b. a -> b
coe T_NonNegative_146
v0 of
      C_constructor_154 Any
v1 -> Any -> Any
forall a b. a -> b
coe Any
v1
      T_NonNegative_146
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Integer.Base.NonPositive
d_NonPositive_158 :: p -> ()
d_NonPositive_158 p
a0 = ()
newtype T_NonPositive_158 = C_constructor_166 AgdaAny
-- Data.Integer.Base.NonPositive.nonPos
d_nonPos_164 :: T_NonPositive_158 -> AgdaAny
d_nonPos_164 :: T_NonPositive_158 -> Any
d_nonPos_164 T_NonPositive_158
v0
  = case T_NonPositive_158 -> T_NonPositive_158
forall a b. a -> b
coe T_NonPositive_158
v0 of
      C_constructor_166 Any
v1 -> Any -> Any
forall a b. a -> b
coe Any
v1
      T_NonPositive_158
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Integer.Base.Negative
d_Negative_170 :: p -> ()
d_Negative_170 p
a0 = ()
newtype T_Negative_170 = C_constructor_178 AgdaAny
-- Data.Integer.Base.Negative.neg
d_neg_176 :: T_Negative_170 -> AgdaAny
d_neg_176 :: T_Negative_170 -> Any
d_neg_176 T_Negative_170
v0
  = case T_Negative_170 -> T_Negative_170
forall a b. a -> b
coe T_Negative_170
v0 of
      C_constructor_178 Any
v1 -> Any -> Any
forall a b. a -> b
coe Any
v1
      T_Negative_170
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Integer.Base.pos
d_pos_182 :: Integer -> T_Positive_134
d_pos_182 :: Integer -> T_Positive_134
d_pos_182 ~Integer
v0 = T_Positive_134
du_pos_182
du_pos_182 :: T_Positive_134
du_pos_182 :: T_Positive_134
du_pos_182
  = (Any -> T_Positive_134) -> Any -> T_Positive_134
forall a b. a -> b
coe Any -> T_Positive_134
C_constructor_142 (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
-- Data.Integer.Base.nonNeg
d_nonNeg_186 :: Integer -> T_NonNegative_146
d_nonNeg_186 :: Integer -> T_NonNegative_146
d_nonNeg_186 ~Integer
v0 = T_NonNegative_146
du_nonNeg_186
du_nonNeg_186 :: T_NonNegative_146
du_nonNeg_186 :: T_NonNegative_146
du_nonNeg_186
  = (Any -> T_NonNegative_146) -> Any -> T_NonNegative_146
forall a b. a -> b
coe Any -> T_NonNegative_146
C_constructor_154 (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
-- Data.Integer.Base.nonPos0
d_nonPos0_188 :: T_NonPositive_158
d_nonPos0_188 :: T_NonPositive_158
d_nonPos0_188
  = (Any -> T_NonPositive_158) -> Any -> T_NonPositive_158
forall a b. a -> b
coe Any -> T_NonPositive_158
C_constructor_166 (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
-- Data.Integer.Base.nonPos
d_nonPos_192 :: Integer -> T_NonPositive_158
d_nonPos_192 :: Integer -> T_NonPositive_158
d_nonPos_192 ~Integer
v0 = T_NonPositive_158
du_nonPos_192
du_nonPos_192 :: T_NonPositive_158
du_nonPos_192 :: T_NonPositive_158
du_nonPos_192
  = (Any -> T_NonPositive_158) -> Any -> T_NonPositive_158
forall a b. a -> b
coe Any -> T_NonPositive_158
C_constructor_166 (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
-- Data.Integer.Base.neg
d_neg_196 :: Integer -> T_Negative_170
d_neg_196 :: Integer -> T_Negative_170
d_neg_196 ~Integer
v0 = T_Negative_170
du_neg_196
du_neg_196 :: T_Negative_170
du_neg_196 :: T_Negative_170
du_neg_196
  = (Any -> T_Negative_170) -> Any -> T_Negative_170
forall a b. a -> b
coe Any -> T_Negative_170
C_constructor_178 (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
-- Data.Integer.Base.≢-nonZero
d_'8802''45'nonZero_200 ::
  Integer ->
  (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Data.Nat.Base.T_NonZero_112
d_'8802''45'nonZero_200 :: Integer -> (T__'8801'__12 -> T_Irrelevant_20) -> T_NonZero_112
d_'8802''45'nonZero_200 Integer
v0 ~T__'8801'__12 -> T_Irrelevant_20
v1 = Integer -> T_NonZero_112
du_'8802''45'nonZero_200 Integer
v0
du_'8802''45'nonZero_200 ::
  Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112
du_'8802''45'nonZero_200 :: Integer -> T_NonZero_112
du_'8802''45'nonZero_200 Integer
v0
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> ((Any -> T_Irrelevant_20) -> Any) -> Any -> T_NonZero_112
forall a b. a -> b
coe
             (Any -> T_Irrelevant_20) -> Any
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
             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 -> T_NonZero_112) -> Any -> T_NonZero_112
forall a b. a -> b
coe
            Any -> T_NonZero_112
MAlonzo.Code.Data.Nat.Base.C_constructor_120
            (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
      Integer
_ -> (Any -> T_NonZero_112) -> Any -> T_NonZero_112
forall a b. a -> b
coe
             Any -> T_NonZero_112
MAlonzo.Code.Data.Nat.Base.C_constructor_120
             (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
-- Data.Integer.Base.>-nonZero
d_'62''45'nonZero_210 ::
  Integer -> T__'60'__50 -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112
d_'62''45'nonZero_210 :: Integer -> T__'60'__50 -> T_NonZero_112
d_'62''45'nonZero_210 ~Integer
v0 T__'60'__50
v1 = T__'60'__50 -> T_NonZero_112
du_'62''45'nonZero_210 T__'60'__50
v1
du_'62''45'nonZero_210 ::
  T__'60'__50 -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112
du_'62''45'nonZero_210 :: T__'60'__50 -> T_NonZero_112
du_'62''45'nonZero_210 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'__22
v3
        -> (Any -> Any -> Any) -> Any -> Any -> T_NonZero_112
forall a b. a -> b
coe
             Any -> Any -> Any
forall a b. a -> b -> b
seq (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v3)
             ((Any -> T_NonZero_112) -> Any -> Any
forall a b. a -> b
coe
                Any -> T_NonZero_112
MAlonzo.Code.Data.Nat.Base.C_constructor_120
                (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))
      T__'60'__50
_ -> T_NonZero_112
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Integer.Base.<-nonZero
d_'60''45'nonZero_216 ::
  Integer -> T__'60'__50 -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112
d_'60''45'nonZero_216 :: Integer -> T__'60'__50 -> T_NonZero_112
d_'60''45'nonZero_216 ~Integer
v0 T__'60'__50
v1 = T__'60'__50 -> T_NonZero_112
du_'60''45'nonZero_216 T__'60'__50
v1
du_'60''45'nonZero_216 ::
  T__'60'__50 -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112
du_'60''45'nonZero_216 :: T__'60'__50 -> T_NonZero_112
du_'60''45'nonZero_216 T__'60'__50
v0
  = (Any -> Any -> Any) -> Any -> Any -> T_NonZero_112
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 -> T_NonZero_112) -> Any -> Any
forall a b. a -> b
coe
         Any -> T_NonZero_112
MAlonzo.Code.Data.Nat.Base.C_constructor_120
         (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))
-- Data.Integer.Base.positive
d_positive_220 :: Integer -> T__'60'__50 -> T_Positive_134
d_positive_220 :: Integer -> T__'60'__50 -> T_Positive_134
d_positive_220 ~Integer
v0 T__'60'__50
v1 = T__'60'__50 -> T_Positive_134
du_positive_220 T__'60'__50
v1
du_positive_220 :: T__'60'__50 -> T_Positive_134
du_positive_220 :: T__'60'__50 -> T_Positive_134
du_positive_220 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'__22
v3
        -> (Any -> Any -> Any) -> Any -> Any -> T_Positive_134
forall a b. a -> b
coe
             Any -> Any -> Any
forall a b. a -> b -> b
seq (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v3)
             ((Any -> T_Positive_134) -> Any -> Any
forall a b. a -> b
coe Any -> T_Positive_134
C_constructor_142 (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))
      T__'60'__50
_ -> T_Positive_134
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Integer.Base.negative
d_negative_226 :: Integer -> T__'60'__50 -> T_Negative_170
d_negative_226 :: Integer -> T__'60'__50 -> T_Negative_170
d_negative_226 ~Integer
v0 T__'60'__50
v1 = T__'60'__50 -> T_Negative_170
du_negative_226 T__'60'__50
v1
du_negative_226 :: T__'60'__50 -> T_Negative_170
du_negative_226 :: T__'60'__50 -> T_Negative_170
du_negative_226 T__'60'__50
v0
  = (Any -> Any -> Any) -> Any -> Any -> T_Negative_170
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 -> T_Negative_170) -> Any -> Any
forall a b. a -> b
coe Any -> T_Negative_170
C_constructor_178 (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))
-- Data.Integer.Base.nonPositive
d_nonPositive_230 :: Integer -> T__'8804'__26 -> T_NonPositive_158
d_nonPositive_230 :: Integer -> T__'8804'__26 -> T_NonPositive_158
d_nonPositive_230 ~Integer
v0 T__'8804'__26
v1 = T__'8804'__26 -> T_NonPositive_158
du_nonPositive_230 T__'8804'__26
v1
du_nonPositive_230 :: T__'8804'__26 -> T_NonPositive_158
du_nonPositive_230 :: T__'8804'__26 -> T_NonPositive_158
du_nonPositive_230 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 -> T_NonPositive_158) -> Any -> T_NonPositive_158
forall a b. a -> b
coe
             Any -> T_NonPositive_158
C_constructor_166 (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
      C_'43''8804''43'_48 T__'8804'__22
v3
        -> (Any -> Any -> Any) -> Any -> Any -> T_NonPositive_158
forall a b. a -> b
coe
             Any -> Any -> Any
forall a b. a -> b -> b
seq (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v3)
             ((Any -> T_NonPositive_158) -> Any -> Any
forall a b. a -> b
coe Any -> T_NonPositive_158
C_constructor_166 (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))
      T__'8804'__26
_ -> T_NonPositive_158
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Integer.Base.nonNegative
d_nonNegative_234 :: Integer -> T__'8804'__26 -> T_NonNegative_146
d_nonNegative_234 :: Integer -> T__'8804'__26 -> T_NonNegative_146
d_nonNegative_234 Integer
v0 ~T__'8804'__26
v1 = Integer -> T_NonNegative_146
du_nonNegative_234 Integer
v0
du_nonNegative_234 :: Integer -> T_NonNegative_146
du_nonNegative_234 :: Integer -> T_NonNegative_146
du_nonNegative_234 Integer
v0
  = (Any -> Any -> Any) -> Any -> Any -> T_NonNegative_146
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 -> T_NonNegative_146) -> Any -> Any
forall a b. a -> b
coe Any -> T_NonNegative_146
C_constructor_154 (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))
-- Data.Integer.Base._◃_
d__'9667'__238 ::
  MAlonzo.Code.Data.Sign.Base.T_Sign_6 -> Integer -> Integer
d__'9667'__238 :: T_Sign_6 -> Integer -> Integer
d__'9667'__238 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_244 :: p -> ()
d_SignAbs_244 p
a0 = ()
data T_SignAbs_244
  = C__'9666'__250 MAlonzo.Code.Data.Sign.Base.T_Sign_6 Integer
-- Data.Integer.Base.signAbs
d_signAbs_254 :: Integer -> T_SignAbs_244
d_signAbs_254 :: Integer -> T_SignAbs_244
d_signAbs_254 Integer
v0
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> (T_Sign_6 -> Integer -> T_SignAbs_244)
-> Any -> Any -> T_SignAbs_244
forall a b. a -> b
coe
             T_Sign_6 -> Integer -> T_SignAbs_244
C__'9666'__250 (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_244)
-> Any -> Any -> T_SignAbs_244
forall a b. a -> b
coe
            T_Sign_6 -> Integer -> T_SignAbs_244
C__'9666'__250 (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_244)
-> Any -> Any -> T_SignAbs_244
forall a b. a -> b
coe
             T_Sign_6 -> Integer -> T_SignAbs_244
C__'9666'__250 (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'__260 :: Integer -> Integer
d_'45'__260 :: Integer -> Integer
d_'45'__260 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'__266 :: Integer -> Integer -> Integer
d__'8854'__266 :: Integer -> Integer -> Integer
d__'8854'__266 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'__260 ((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'__284 :: Integer -> Integer -> Integer
d__'43'__284 :: Integer -> Integer -> Integer
d__'43'__284 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'__266 (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'__266 (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'__302 :: Integer -> Integer -> Integer
d__'45'__302 :: Integer -> Integer -> Integer
d__'45'__302 Integer
v0 Integer
v1
  = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
d__'43'__284 (Integer -> Any
forall a b. a -> b
coe Integer
v0) ((Integer -> Integer) -> Any -> Any
forall a b. a -> b
coe Integer -> Integer
d_'45'__260 (Integer -> Any
forall a b. a -> b
coe Integer
v1))
-- Data.Integer.Base.suc
d_suc_308 :: Integer -> Integer
d_suc_308 :: Integer -> Integer
d_suc_308 Integer
v0 = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
d__'43'__284 (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_312 :: Integer -> Integer
d_pred_312 :: Integer -> Integer
d_pred_312 Integer
v0 = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
d__'43'__284 (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'__316 :: Integer -> Integer -> Integer
d__'42'__316 :: Integer -> Integer -> Integer
d__'42'__316 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'__238
      ((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__'94'__322 :: Integer -> Integer -> Integer
d__'94'__322 :: Integer -> Integer -> Integer
d__'94'__322 Integer
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
d_1ℤ_16
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> Integer
forall a b. a -> b
coe
             ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
d__'42'__316 (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
d__'94'__322 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
-- Data.Integer.Base._⊔_
d__'8852'__330 :: Integer -> Integer -> Integer
d__'8852'__330 :: Integer -> Integer -> Integer
d__'8852'__330 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'__208 (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'__236 (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'__348 :: Integer -> Integer -> Integer
d__'8851'__348 :: Integer -> Integer -> Integer
d__'8851'__348 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'__236 (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'__208 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3))))
-- Data.Integer.Base._/ℕ_
d__'47'ℕ__372 ::
  Integer ->
  Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d__'47'ℕ__372 :: Integer -> Integer -> T_NonZero_112 -> Integer
d__'47'ℕ__372 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> Integer
du__'47'ℕ__372 Integer
v0 Integer
v1
du__'47'ℕ__372 :: Integer -> Integer -> Integer
du__'47'ℕ__372 :: Integer -> Integer -> Integer
du__'47'ℕ__372 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)) ->
          (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__318 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
      Any
_ -> let v2 :: Any
v2
                 = (Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                     Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__330
                     ((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)) (Integer -> Any
forall a b. a -> b
coe Integer
v1) in
           Any -> Integer
forall a b. a -> b
coe
             (case Any -> Integer
forall a b. a -> b
coe Any
v2 of
                Integer
0 -> (Integer -> Integer) -> Any -> Any
forall a b. a -> b
coe
                       Integer -> Integer
d_'45'__260
                       ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                          Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__318
                          ((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)) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
                Integer
_ -> (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.du__'47'__318
                          ((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)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
-- Data.Integer.Base._/_
d__'47'__402 ::
  Integer ->
  Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d__'47'__402 :: Integer -> Integer -> T_NonZero_112 -> Integer
d__'47'__402 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> Integer
du__'47'__402 Integer
v0 Integer
v1
du__'47'__402 :: Integer -> Integer -> Integer
du__'47'__402 :: Integer -> Integer -> Integer
du__'47'__402 Integer
v0 Integer
v1
  = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
      Integer -> Integer -> Integer
d__'42'__316
      ((T_Sign_6 -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe T_Sign_6 -> Integer -> Integer
d__'9667'__238 ((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 -> 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
du__'47'ℕ__372 (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__'37'ℕ__414 ::
  Integer ->
  Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d__'37'ℕ__414 :: Integer -> Integer -> T_NonZero_112 -> Integer
d__'37'ℕ__414 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> Integer
du__'37'ℕ__414 Integer
v0 Integer
v1
du__'37'ℕ__414 :: Integer -> Integer -> Integer
du__'37'ℕ__414 :: Integer -> Integer -> Integer
du__'37'ℕ__414 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)) ->
          (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__330 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
      Any
_ -> let v2 :: Any
v2
                 = (Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                     Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__330
                     ((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)) (Integer -> Any
forall a b. a -> b
coe Integer
v1) in
           Any -> Integer
forall a b. a -> b
coe
             (case Any -> Integer
forall a b. a -> b
coe Any
v2 of
                Integer
0 -> Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)
                Integer
_ -> (Integer -> Integer -> Integer) -> Integer -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22 Integer
v1 Any
v2)
-- Data.Integer.Base._%_
d__'37'__444 ::
  Integer ->
  Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d__'37'__444 :: Integer -> Integer -> T_NonZero_112 -> Integer
d__'37'__444 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> Integer
du__'37'__444 Integer
v0 Integer
v1
du__'37'__444 :: Integer -> Integer -> Integer
du__'37'__444 :: Integer -> Integer -> Integer
du__'37'__444 Integer
v0 Integer
v1
  = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
du__'37'ℕ__414 (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.+-rawMagma
d_'43''45'rawMagma_450 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawMagma_44
d_'43''45'rawMagma_450 :: T_RawMagma_44
d_'43''45'rawMagma_450
  = ((Any -> Any -> Any) -> T_RawMagma_44)
-> (Integer -> Integer -> Integer) -> T_RawMagma_44
forall a b. a -> b
coe
      (Any -> Any -> Any) -> T_RawMagma_44
MAlonzo.Code.Algebra.Bundles.Raw.C_constructor_68 Integer -> Integer -> Integer
d__'43'__284
-- Data.Integer.Base.+-0-rawMonoid
d_'43''45'0'45'rawMonoid_452 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawMonoid_74
d_'43''45'0'45'rawMonoid_452 :: T_RawMonoid_74
d_'43''45'0'45'rawMonoid_452
  = ((Any -> Any -> Any) -> Any -> T_RawMonoid_74)
-> (Integer -> Integer -> Integer) -> Integer -> T_RawMonoid_74
forall a b. a -> b
coe
      (Any -> Any -> Any) -> Any -> T_RawMonoid_74
MAlonzo.Code.Algebra.Bundles.Raw.C_constructor_102 Integer -> Integer -> Integer
d__'43'__284
      Integer
d_0ℤ_12
-- Data.Integer.Base.+-0-rawGroup
d_'43''45'0'45'rawGroup_454 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawGroup_108
d_'43''45'0'45'rawGroup_454 :: T_RawGroup_108
d_'43''45'0'45'rawGroup_454
  = ((Any -> Any -> Any) -> Any -> (Any -> Any) -> T_RawGroup_108)
-> (Integer -> Integer -> Integer)
-> Integer
-> (Integer -> Integer)
-> T_RawGroup_108
forall a b. a -> b
coe
      (Any -> Any -> Any) -> Any -> (Any -> Any) -> T_RawGroup_108
MAlonzo.Code.Algebra.Bundles.Raw.C_constructor_142 Integer -> Integer -> Integer
d__'43'__284
      Integer
d_0ℤ_12 Integer -> Integer
d_'45'__260
-- Data.Integer.Base.*-rawMagma
d_'42''45'rawMagma_456 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawMagma_44
d_'42''45'rawMagma_456 :: T_RawMagma_44
d_'42''45'rawMagma_456
  = ((Any -> Any -> Any) -> T_RawMagma_44)
-> (Integer -> Integer -> Integer) -> T_RawMagma_44
forall a b. a -> b
coe
      (Any -> Any -> Any) -> T_RawMagma_44
MAlonzo.Code.Algebra.Bundles.Raw.C_constructor_68 Integer -> Integer -> Integer
d__'42'__316
-- Data.Integer.Base.*-1-rawMonoid
d_'42''45'1'45'rawMonoid_458 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawMonoid_74
d_'42''45'1'45'rawMonoid_458 :: T_RawMonoid_74
d_'42''45'1'45'rawMonoid_458
  = ((Any -> Any -> Any) -> Any -> T_RawMonoid_74)
-> (Integer -> Integer -> Integer) -> Integer -> T_RawMonoid_74
forall a b. a -> b
coe
      (Any -> Any -> Any) -> Any -> T_RawMonoid_74
MAlonzo.Code.Algebra.Bundles.Raw.C_constructor_102 Integer -> Integer -> Integer
d__'42'__316
      Integer
d_1ℤ_16
-- Data.Integer.Base.+-*-rawNearSemiring
d_'43''45''42''45'rawNearSemiring_460 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawNearSemiring_148
d_'43''45''42''45'rawNearSemiring_460 :: T_RawNearSemiring_148
d_'43''45''42''45'rawNearSemiring_460
  = ((Any -> Any -> Any)
 -> (Any -> Any -> Any) -> Any -> T_RawNearSemiring_148)
-> (Integer -> Integer -> Integer)
-> (Integer -> Integer -> Integer)
-> Integer
-> T_RawNearSemiring_148
forall a b. a -> b
coe
      (Any -> Any -> Any)
-> (Any -> Any -> Any) -> Any -> T_RawNearSemiring_148
MAlonzo.Code.Algebra.Bundles.Raw.C_constructor_184 Integer -> Integer -> Integer
d__'43'__284
      Integer -> Integer -> Integer
d__'42'__316 Integer
d_0ℤ_12
-- Data.Integer.Base.+-*-rawSemiring
d_'43''45''42''45'rawSemiring_462 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawSemiring_190
d_'43''45''42''45'rawSemiring_462 :: T_RawSemiring_190
d_'43''45''42''45'rawSemiring_462
  = ((Any -> Any -> Any)
 -> (Any -> Any -> Any) -> Any -> Any -> T_RawSemiring_190)
-> (Integer -> Integer -> Integer)
-> (Integer -> Integer -> Integer)
-> Integer
-> Integer
-> T_RawSemiring_190
forall a b. a -> b
coe
      (Any -> Any -> Any)
-> (Any -> Any -> Any) -> Any -> Any -> T_RawSemiring_190
MAlonzo.Code.Algebra.Bundles.Raw.C_constructor_234 Integer -> Integer -> Integer
d__'43'__284
      Integer -> Integer -> Integer
d__'42'__316 Integer
d_0ℤ_12 Integer
d_1ℤ_16
-- Data.Integer.Base.+-*-rawRing
d_'43''45''42''45'rawRing_464 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawRing_290
d_'43''45''42''45'rawRing_464 :: T_RawRing_290
d_'43''45''42''45'rawRing_464
  = ((Any -> Any -> Any)
 -> (Any -> Any -> Any)
 -> (Any -> Any)
 -> Any
 -> Any
 -> T_RawRing_290)
-> (Integer -> Integer -> Integer)
-> (Integer -> Integer -> Integer)
-> (Integer -> Integer)
-> Integer
-> Integer
-> T_RawRing_290
forall a b. a -> b
coe
      (Any -> Any -> Any)
-> (Any -> Any -> Any)
-> (Any -> Any)
-> Any
-> Any
-> T_RawRing_290
MAlonzo.Code.Algebra.Bundles.Raw.C_constructor_344 Integer -> Integer -> Integer
d__'43'__284
      Integer -> Integer -> Integer
d__'42'__316 Integer -> Integer
d_'45'__260 Integer
d_0ℤ_12 Integer
d_1ℤ_16