{-# 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_Positive'46'constructor_1399 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_Positive'46'constructor_1399 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_144 :: p -> ()
d_NonNegative_144 p
a0 = ()
newtype T_NonNegative_144
  = C_NonNegative'46'constructor_1457 AgdaAny
-- Data.Integer.Base.NonNegative.nonNeg
d_nonNeg_150 :: T_NonNegative_144 -> AgdaAny
d_nonNeg_150 :: T_NonNegative_144 -> Any
d_nonNeg_150 T_NonNegative_144
v0
  = case T_NonNegative_144 -> T_NonNegative_144
forall a b. a -> b
coe T_NonNegative_144
v0 of
      C_NonNegative'46'constructor_1457 Any
v1 -> Any -> Any
forall a b. a -> b
coe Any
v1
      T_NonNegative_144
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Integer.Base.NonPositive
d_NonPositive_154 :: p -> ()
d_NonPositive_154 p
a0 = ()
newtype T_NonPositive_154
  = C_NonPositive'46'constructor_1515 AgdaAny
-- Data.Integer.Base.NonPositive.nonPos
d_nonPos_160 :: T_NonPositive_154 -> AgdaAny
d_nonPos_160 :: T_NonPositive_154 -> Any
d_nonPos_160 T_NonPositive_154
v0
  = case T_NonPositive_154 -> T_NonPositive_154
forall a b. a -> b
coe T_NonPositive_154
v0 of
      C_NonPositive'46'constructor_1515 Any
v1 -> Any -> Any
forall a b. a -> b
coe Any
v1
      T_NonPositive_154
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Integer.Base.Negative
d_Negative_164 :: p -> ()
d_Negative_164 p
a0 = ()
newtype T_Negative_164 = C_Negative'46'constructor_1573 AgdaAny
-- Data.Integer.Base.Negative.neg
d_neg_170 :: T_Negative_164 -> AgdaAny
d_neg_170 :: T_Negative_164 -> Any
d_neg_170 T_Negative_164
v0
  = case T_Negative_164 -> T_Negative_164
forall a b. a -> b
coe T_Negative_164
v0 of
      C_Negative'46'constructor_1573 Any
v1 -> Any -> Any
forall a b. a -> b
coe Any
v1
      T_Negative_164
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Integer.Base.pos
d_pos_174 :: Integer -> T_Positive_134
d_pos_174 :: Integer -> T_Positive_134
d_pos_174 ~Integer
v0 = T_Positive_134
du_pos_174
du_pos_174 :: T_Positive_134
du_pos_174 :: T_Positive_134
du_pos_174
  = (Any -> T_Positive_134) -> Any -> T_Positive_134
forall a b. a -> b
coe
      Any -> T_Positive_134
C_Positive'46'constructor_1399
      (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
-- Data.Integer.Base.nonNeg
d_nonNeg_178 :: Integer -> T_NonNegative_144
d_nonNeg_178 :: Integer -> T_NonNegative_144
d_nonNeg_178 ~Integer
v0 = T_NonNegative_144
du_nonNeg_178
du_nonNeg_178 :: T_NonNegative_144
du_nonNeg_178 :: T_NonNegative_144
du_nonNeg_178
  = (Any -> T_NonNegative_144) -> Any -> T_NonNegative_144
forall a b. a -> b
coe
      Any -> T_NonNegative_144
C_NonNegative'46'constructor_1457
      (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
-- Data.Integer.Base.nonPos0
d_nonPos0_180 :: T_NonPositive_154
d_nonPos0_180 :: T_NonPositive_154
d_nonPos0_180
  = (Any -> T_NonPositive_154) -> Any -> T_NonPositive_154
forall a b. a -> b
coe
      Any -> T_NonPositive_154
C_NonPositive'46'constructor_1515
      (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
-- Data.Integer.Base.nonPos
d_nonPos_184 :: Integer -> T_NonPositive_154
d_nonPos_184 :: Integer -> T_NonPositive_154
d_nonPos_184 ~Integer
v0 = T_NonPositive_154
du_nonPos_184
du_nonPos_184 :: T_NonPositive_154
du_nonPos_184 :: T_NonPositive_154
du_nonPos_184
  = (Any -> T_NonPositive_154) -> Any -> T_NonPositive_154
forall a b. a -> b
coe
      Any -> T_NonPositive_154
C_NonPositive'46'constructor_1515
      (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
-- Data.Integer.Base.neg
d_neg_188 :: Integer -> T_Negative_164
d_neg_188 :: Integer -> T_Negative_164
d_neg_188 ~Integer
v0 = T_Negative_164
du_neg_188
du_neg_188 :: T_Negative_164
du_neg_188 :: T_Negative_164
du_neg_188
  = (Any -> T_Negative_164) -> Any -> T_Negative_164
forall a b. a -> b
coe
      Any -> T_Negative_164
C_Negative'46'constructor_1573
      (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
-- Data.Integer.Base.≢-nonZero
d_'8802''45'nonZero_192 ::
  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_192 :: Integer -> (T__'8801'__12 -> T_Irrelevant_20) -> T_NonZero_112
d_'8802''45'nonZero_192 Integer
v0 ~T__'8801'__12 -> T_Irrelevant_20
v1 = Integer -> T_NonZero_112
du_'8802''45'nonZero_192 Integer
v0
du_'8802''45'nonZero_192 ::
  Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112
du_'8802''45'nonZero_192 :: Integer -> T_NonZero_112
du_'8802''45'nonZero_192 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_NonZero'46'constructor_3575
            (() -> 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_NonZero'46'constructor_3575
             (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
-- Data.Integer.Base.>-nonZero
d_'62''45'nonZero_202 ::
  Integer -> T__'60'__50 -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112
d_'62''45'nonZero_202 :: Integer -> T__'60'__50 -> T_NonZero_112
d_'62''45'nonZero_202 ~Integer
v0 T__'60'__50
v1 = T__'60'__50 -> T_NonZero_112
du_'62''45'nonZero_202 T__'60'__50
v1
du_'62''45'nonZero_202 ::
  T__'60'__50 -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112
du_'62''45'nonZero_202 :: T__'60'__50 -> T_NonZero_112
du_'62''45'nonZero_202 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_NonZero'46'constructor_3575
                (() -> 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_208 ::
  Integer -> T__'60'__50 -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112
d_'60''45'nonZero_208 :: Integer -> T__'60'__50 -> T_NonZero_112
d_'60''45'nonZero_208 ~Integer
v0 T__'60'__50
v1 = T__'60'__50 -> T_NonZero_112
du_'60''45'nonZero_208 T__'60'__50
v1
du_'60''45'nonZero_208 ::
  T__'60'__50 -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112
du_'60''45'nonZero_208 :: T__'60'__50 -> T_NonZero_112
du_'60''45'nonZero_208 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_NonZero'46'constructor_3575
         (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))
-- Data.Integer.Base.positive
d_positive_212 :: Integer -> T__'60'__50 -> T_Positive_134
d_positive_212 :: Integer -> T__'60'__50 -> T_Positive_134
d_positive_212 ~Integer
v0 T__'60'__50
v1 = T__'60'__50 -> T_Positive_134
du_positive_212 T__'60'__50
v1
du_positive_212 :: T__'60'__50 -> T_Positive_134
du_positive_212 :: T__'60'__50 -> T_Positive_134
du_positive_212 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_Positive'46'constructor_1399
                (() -> 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_218 :: Integer -> T__'60'__50 -> T_Negative_164
d_negative_218 :: Integer -> T__'60'__50 -> T_Negative_164
d_negative_218 ~Integer
v0 T__'60'__50
v1 = T__'60'__50 -> T_Negative_164
du_negative_218 T__'60'__50
v1
du_negative_218 :: T__'60'__50 -> T_Negative_164
du_negative_218 :: T__'60'__50 -> T_Negative_164
du_negative_218 T__'60'__50
v0
  = (Any -> Any -> Any) -> Any -> Any -> T_Negative_164
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_164) -> Any -> Any
forall a b. a -> b
coe
         Any -> T_Negative_164
C_Negative'46'constructor_1573
         (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))
-- Data.Integer.Base.nonPositive
d_nonPositive_222 :: Integer -> T__'8804'__26 -> T_NonPositive_154
d_nonPositive_222 :: Integer -> T__'8804'__26 -> T_NonPositive_154
d_nonPositive_222 ~Integer
v0 T__'8804'__26
v1 = T__'8804'__26 -> T_NonPositive_154
du_nonPositive_222 T__'8804'__26
v1
du_nonPositive_222 :: T__'8804'__26 -> T_NonPositive_154
du_nonPositive_222 :: T__'8804'__26 -> T_NonPositive_154
du_nonPositive_222 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_154) -> Any -> T_NonPositive_154
forall a b. a -> b
coe
             Any -> T_NonPositive_154
C_NonPositive'46'constructor_1515
             (() -> 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_154
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_154) -> Any -> Any
forall a b. a -> b
coe
                Any -> T_NonPositive_154
C_NonPositive'46'constructor_1515
                (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))
      T__'8804'__26
_ -> T_NonPositive_154
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Integer.Base.nonNegative
d_nonNegative_226 :: Integer -> T__'8804'__26 -> T_NonNegative_144
d_nonNegative_226 :: Integer -> T__'8804'__26 -> T_NonNegative_144
d_nonNegative_226 Integer
v0 ~T__'8804'__26
v1 = Integer -> T_NonNegative_144
du_nonNegative_226 Integer
v0
du_nonNegative_226 :: Integer -> T_NonNegative_144
du_nonNegative_226 :: Integer -> T_NonNegative_144
du_nonNegative_226 Integer
v0
  = (Any -> Any -> Any) -> Any -> Any -> T_NonNegative_144
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_144) -> Any -> Any
forall a b. a -> b
coe
         Any -> T_NonNegative_144
C_NonNegative'46'constructor_1457
         (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))
-- Data.Integer.Base._◃_
d__'9667'__230 ::
  MAlonzo.Code.Data.Sign.Base.T_Sign_6 -> Integer -> Integer
d__'9667'__230 :: T_Sign_6 -> Integer -> Integer
d__'9667'__230 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_236 :: p -> ()
d_SignAbs_236 p
a0 = ()
data T_SignAbs_236
  = C__'9666'__242 MAlonzo.Code.Data.Sign.Base.T_Sign_6 Integer
-- Data.Integer.Base.signAbs
d_signAbs_246 :: Integer -> T_SignAbs_236
d_signAbs_246 :: Integer -> T_SignAbs_236
d_signAbs_246 Integer
v0
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> (T_Sign_6 -> Integer -> T_SignAbs_236)
-> Any -> Any -> T_SignAbs_236
forall a b. a -> b
coe
             T_Sign_6 -> Integer -> T_SignAbs_236
C__'9666'__242 (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_236)
-> Any -> Any -> T_SignAbs_236
forall a b. a -> b
coe
            T_Sign_6 -> Integer -> T_SignAbs_236
C__'9666'__242 (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_236)
-> Any -> Any -> T_SignAbs_236
forall a b. a -> b
coe
             T_Sign_6 -> Integer -> T_SignAbs_236
C__'9666'__242 (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'__252 :: Integer -> Integer
d_'45'__252 :: Integer -> Integer
d_'45'__252 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'__258 :: Integer -> Integer -> Integer
d__'8854'__258 :: Integer -> Integer -> Integer
d__'8854'__258 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'__252 ((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'__276 :: Integer -> Integer -> Integer
d__'43'__276 :: Integer -> Integer -> Integer
d__'43'__276 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'__258 (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'__258 (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'__294 :: Integer -> Integer -> Integer
d__'45'__294 :: Integer -> Integer -> Integer
d__'45'__294 Integer
v0 Integer
v1
  = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
d__'43'__276 (Integer -> Any
forall a b. a -> b
coe Integer
v0) ((Integer -> Integer) -> Any -> Any
forall a b. a -> b
coe Integer -> Integer
d_'45'__252 (Integer -> Any
forall a b. a -> b
coe Integer
v1))
-- Data.Integer.Base.suc
d_suc_300 :: Integer -> Integer
d_suc_300 :: Integer -> Integer
d_suc_300 Integer
v0 = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
d__'43'__276 (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_304 :: Integer -> Integer
d_pred_304 :: Integer -> Integer
d_pred_304 Integer
v0 = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
d__'43'__276 (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'__308 :: Integer -> Integer -> Integer
d__'42'__308 :: Integer -> Integer -> Integer
d__'42'__308 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'__230
      ((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'__314 :: Integer -> Integer -> Integer
d__'94'__314 :: Integer -> Integer -> Integer
d__'94'__314 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'__308 (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'__314 (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'__322 :: Integer -> Integer -> Integer
d__'8852'__322 :: Integer -> Integer -> Integer
d__'8852'__322 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'__204 (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'__232 (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'__340 :: Integer -> Integer -> Integer
d__'8851'__340 :: Integer -> Integer -> Integer
d__'8851'__340 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'__232 (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'__204 (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'ℕ__364 ::
  Integer ->
  Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d__'47'ℕ__364 :: Integer -> Integer -> T_NonZero_112 -> Integer
d__'47'ℕ__364 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> Integer
du__'47'ℕ__364 Integer
v0 Integer
v1
du__'47'ℕ__364 :: Integer -> Integer -> Integer
du__'47'ℕ__364 :: Integer -> Integer -> Integer
du__'47'ℕ__364 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'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
      Any
_ -> let v2 :: t
v2
                 = (Integer -> Integer -> Integer) -> Any -> Any -> t
forall a b. a -> b
coe
                     Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326
                     ((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
forall a. a
v2 of
                Integer
0 -> (Integer -> Integer) -> Any -> Any
forall a b. a -> b
coe
                       Integer -> Integer
d_'45'__252
                       ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                          Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314
                          ((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'__314
                          ((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'__394 ::
  Integer ->
  Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d__'47'__394 :: Integer -> Integer -> T_NonZero_112 -> Integer
d__'47'__394 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> Integer
du__'47'__394 Integer
v0 Integer
v1
du__'47'__394 :: Integer -> Integer -> Integer
du__'47'__394 :: Integer -> Integer -> Integer
du__'47'__394 Integer
v0 Integer
v1
  = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
      Integer -> Integer -> Integer
d__'42'__308
      ((T_Sign_6 -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe T_Sign_6 -> Integer -> Integer
d__'9667'__230 ((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'ℕ__364 (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'ℕ__406 ::
  Integer ->
  Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d__'37'ℕ__406 :: Integer -> Integer -> T_NonZero_112 -> Integer
d__'37'ℕ__406 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> Integer
du__'37'ℕ__406 Integer
v0 Integer
v1
du__'37'ℕ__406 :: Integer -> Integer -> Integer
du__'37'ℕ__406 :: Integer -> Integer -> Integer
du__'37'ℕ__406 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'__326 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
      Any
_ -> let v2 :: t
v2
                 = (Integer -> Integer -> Integer) -> Any -> Any -> t
forall a b. a -> b
coe
                     Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326
                     ((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
forall a. a
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
forall a. a
v2)
-- Data.Integer.Base._%_
d__'37'__436 ::
  Integer ->
  Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d__'37'__436 :: Integer -> Integer -> T_NonZero_112 -> Integer
d__'37'__436 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> Integer
du__'37'__436 Integer
v0 Integer
v1
du__'37'__436 :: Integer -> Integer -> Integer
du__'37'__436 :: Integer -> Integer -> Integer
du__'37'__436 Integer
v0 Integer
v1
  = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
du__'37'ℕ__406 (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_442 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawMagma_36
d_'43''45'rawMagma_442 :: T_RawMagma_36
d_'43''45'rawMagma_442
  = ((Any -> Any -> Any) -> T_RawMagma_36)
-> (Integer -> Integer -> Integer) -> T_RawMagma_36
forall a b. a -> b
coe
      (Any -> Any -> Any) -> T_RawMagma_36
MAlonzo.Code.Algebra.Bundles.Raw.C_RawMagma'46'constructor_341
      Integer -> Integer -> Integer
d__'43'__276
-- Data.Integer.Base.+-0-rawMonoid
d_'43''45'0'45'rawMonoid_444 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawMonoid_64
d_'43''45'0'45'rawMonoid_444 :: T_RawMonoid_64
d_'43''45'0'45'rawMonoid_444
  = ((Any -> Any -> Any) -> Any -> T_RawMonoid_64)
-> (Integer -> Integer -> Integer) -> Integer -> T_RawMonoid_64
forall a b. a -> b
coe
      (Any -> Any -> Any) -> Any -> T_RawMonoid_64
MAlonzo.Code.Algebra.Bundles.Raw.C_RawMonoid'46'constructor_745
      Integer -> Integer -> Integer
d__'43'__276 Integer
d_0ℤ_12
-- Data.Integer.Base.+-0-rawGroup
d_'43''45'0'45'rawGroup_446 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawGroup_96
d_'43''45'0'45'rawGroup_446 :: T_RawGroup_96
d_'43''45'0'45'rawGroup_446
  = ((Any -> Any -> Any) -> Any -> (Any -> Any) -> T_RawGroup_96)
-> (Integer -> Integer -> Integer)
-> Integer
-> (Integer -> Integer)
-> T_RawGroup_96
forall a b. a -> b
coe
      (Any -> Any -> Any) -> Any -> (Any -> Any) -> T_RawGroup_96
MAlonzo.Code.Algebra.Bundles.Raw.C_RawGroup'46'constructor_1207
      Integer -> Integer -> Integer
d__'43'__276 Integer
d_0ℤ_12 Integer -> Integer
d_'45'__252
-- Data.Integer.Base.*-rawMagma
d_'42''45'rawMagma_448 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawMagma_36
d_'42''45'rawMagma_448 :: T_RawMagma_36
d_'42''45'rawMagma_448
  = ((Any -> Any -> Any) -> T_RawMagma_36)
-> (Integer -> Integer -> Integer) -> T_RawMagma_36
forall a b. a -> b
coe
      (Any -> Any -> Any) -> T_RawMagma_36
MAlonzo.Code.Algebra.Bundles.Raw.C_RawMagma'46'constructor_341
      Integer -> Integer -> Integer
d__'42'__308
-- Data.Integer.Base.*-1-rawMonoid
d_'42''45'1'45'rawMonoid_450 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawMonoid_64
d_'42''45'1'45'rawMonoid_450 :: T_RawMonoid_64
d_'42''45'1'45'rawMonoid_450
  = ((Any -> Any -> Any) -> Any -> T_RawMonoid_64)
-> (Integer -> Integer -> Integer) -> Integer -> T_RawMonoid_64
forall a b. a -> b
coe
      (Any -> Any -> Any) -> Any -> T_RawMonoid_64
MAlonzo.Code.Algebra.Bundles.Raw.C_RawMonoid'46'constructor_745
      Integer -> Integer -> Integer
d__'42'__308 Integer
d_1ℤ_16
-- Data.Integer.Base.+-*-rawNearSemiring
d_'43''45''42''45'rawNearSemiring_452 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawNearSemiring_134
d_'43''45''42''45'rawNearSemiring_452 :: T_RawNearSemiring_134
d_'43''45''42''45'rawNearSemiring_452
  = ((Any -> Any -> Any)
 -> (Any -> Any -> Any) -> Any -> T_RawNearSemiring_134)
-> (Integer -> Integer -> Integer)
-> (Integer -> Integer -> Integer)
-> Integer
-> T_RawNearSemiring_134
forall a b. a -> b
coe
      (Any -> Any -> Any)
-> (Any -> Any -> Any) -> Any -> T_RawNearSemiring_134
MAlonzo.Code.Algebra.Bundles.Raw.C_RawNearSemiring'46'constructor_1729
      Integer -> Integer -> Integer
d__'43'__276 Integer -> Integer -> Integer
d__'42'__308 Integer
d_0ℤ_12
-- Data.Integer.Base.+-*-rawSemiring
d_'43''45''42''45'rawSemiring_454 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawSemiring_174
d_'43''45''42''45'rawSemiring_454 :: T_RawSemiring_174
d_'43''45''42''45'rawSemiring_454
  = ((Any -> Any -> Any)
 -> (Any -> Any -> Any) -> Any -> Any -> T_RawSemiring_174)
-> (Integer -> Integer -> Integer)
-> (Integer -> Integer -> Integer)
-> Integer
-> Integer
-> T_RawSemiring_174
forall a b. a -> b
coe
      (Any -> Any -> Any)
-> (Any -> Any -> Any) -> Any -> Any -> T_RawSemiring_174
MAlonzo.Code.Algebra.Bundles.Raw.C_RawSemiring'46'constructor_2353
      Integer -> Integer -> Integer
d__'43'__276 Integer -> Integer -> Integer
d__'42'__308 Integer
d_0ℤ_12 Integer
d_1ℤ_16
-- Data.Integer.Base.+-*-rawRing
d_'43''45''42''45'rawRing_456 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawRing_268
d_'43''45''42''45'rawRing_456 :: T_RawRing_268
d_'43''45''42''45'rawRing_456
  = ((Any -> Any -> Any)
 -> (Any -> Any -> Any)
 -> (Any -> Any)
 -> Any
 -> Any
 -> T_RawRing_268)
-> (Integer -> Integer -> Integer)
-> (Integer -> Integer -> Integer)
-> (Integer -> Integer)
-> Integer
-> Integer
-> T_RawRing_268
forall a b. a -> b
coe
      (Any -> Any -> Any)
-> (Any -> Any -> Any)
-> (Any -> Any)
-> Any
-> Any
-> T_RawRing_268
MAlonzo.Code.Algebra.Bundles.Raw.C_RawRing'46'constructor_3857
      Integer -> Integer -> Integer
d__'43'__276 Integer -> Integer -> Integer
d__'42'__308 Integer -> Integer
d_'45'__252 Integer
d_0ℤ_12 Integer
d_1ℤ_16