{-# 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.Nat.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.Algebra.Definitions.RawMagma
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.Parity.Base
import qualified MAlonzo.Code.Relation.Nullary.Negation.Core

-- Data.Nat.Base._≤ᵇ_
d__'8804''7495'__14 :: Integer -> Integer -> Bool
d__'8804''7495'__14 :: Integer -> Integer -> Bool
d__'8804''7495'__14 Integer
v0 Integer
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> Bool -> Bool
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> Bool
forall a b. a -> b
coe ((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Bool
ltInt (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
-- Data.Nat.Base._≤_
d__'8804'__22 :: p -> p -> ()
d__'8804'__22 p
a0 p
a1 = ()
data T__'8804'__22 = C_z'8804'n_26 | C_s'8804's_34 T__'8804'__22
-- Data.Nat.Base._<_
d__'60'__36 :: Integer -> Integer -> ()
d__'60'__36 :: Integer -> Integer -> ()
d__'60'__36 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base.s≤s⁻¹
d_s'8804's'8315''185'_62 ::
  Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
d_s'8804's'8315''185'_62 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
d_s'8804's'8315''185'_62 ~Integer
v0 ~Integer
v1 T__'8804'__22
v2 = T__'8804'__22 -> T__'8804'__22
du_s'8804's'8315''185'_62 T__'8804'__22
v2
du_s'8804's'8315''185'_62 :: T__'8804'__22 -> T__'8804'__22
du_s'8804's'8315''185'_62 :: T__'8804'__22 -> T__'8804'__22
du_s'8804's'8315''185'_62 T__'8804'__22
v0
  = case T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22
v0 of
      C_s'8804's_34 T__'8804'__22
v3 -> T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22
v3
      T__'8804'__22
_ -> T__'8804'__22
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Base.s<s⁻¹
d_s'60's'8315''185'_70 ::
  Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
d_s'60's'8315''185'_70 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
d_s'60's'8315''185'_70 ~Integer
v0 ~Integer
v1 T__'8804'__22
v2 = T__'8804'__22 -> T__'8804'__22
du_s'60's'8315''185'_70 T__'8804'__22
v2
du_s'60's'8315''185'_70 :: T__'8804'__22 -> T__'8804'__22
du_s'60's'8315''185'_70 :: T__'8804'__22 -> T__'8804'__22
du_s'60's'8315''185'_70 T__'8804'__22
v0
  = case T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22
v0 of
      C_s'8804's_34 T__'8804'__22
v3 -> T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22
v3
      T__'8804'__22
_ -> T__'8804'__22
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Base._≥_
d__'8805'__74 :: Integer -> Integer -> ()
d__'8805'__74 :: Integer -> Integer -> ()
d__'8805'__74 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._>_
d__'62'__80 :: Integer -> Integer -> ()
d__'62'__80 :: Integer -> Integer -> ()
d__'62'__80 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._≰_
d__'8816'__86 :: Integer -> Integer -> ()
d__'8816'__86 :: Integer -> Integer -> ()
d__'8816'__86 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._≮_
d__'8814'__92 :: Integer -> Integer -> ()
d__'8814'__92 :: Integer -> Integer -> ()
d__'8814'__92 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._≱_
d__'8817'__98 :: Integer -> Integer -> ()
d__'8817'__98 :: Integer -> Integer -> ()
d__'8817'__98 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._≯_
d__'8815'__104 :: Integer -> Integer -> ()
d__'8815'__104 :: Integer -> Integer -> ()
d__'8815'__104 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base.NonZero
d_NonZero_112 :: p -> ()
d_NonZero_112 p
a0 = ()
newtype T_NonZero_112 = C_NonZero'46'constructor_3575 AgdaAny
-- Data.Nat.Base.NonZero.nonZero
d_nonZero_118 :: T_NonZero_112 -> AgdaAny
d_nonZero_118 :: T_NonZero_112 -> Any
d_nonZero_118 T_NonZero_112
v0
  = case T_NonZero_112 -> T_NonZero_112
forall a b. a -> b
coe T_NonZero_112
v0 of
      C_NonZero'46'constructor_3575 Any
v1 -> Any -> Any
forall a b. a -> b
coe Any
v1
      T_NonZero_112
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Base.nonZero
d_nonZero_122 :: Integer -> T_NonZero_112
d_nonZero_122 :: Integer -> T_NonZero_112
d_nonZero_122 ~Integer
v0 = T_NonZero_112
du_nonZero_122
du_nonZero_122 :: T_NonZero_112
du_nonZero_122 :: T_NonZero_112
du_nonZero_122
  = (Any -> T_NonZero_112) -> Any -> T_NonZero_112
forall a b. a -> b
coe
      Any -> T_NonZero_112
C_NonZero'46'constructor_3575
      (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
-- Data.Nat.Base.≢-nonZero
d_'8802''45'nonZero_126 ::
  Integer ->
  (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  T_NonZero_112
d_'8802''45'nonZero_126 :: Integer -> (T__'8801'__12 -> T_Irrelevant_20) -> T_NonZero_112
d_'8802''45'nonZero_126 Integer
v0 ~T__'8801'__12 -> T_Irrelevant_20
v1 = Integer -> T_NonZero_112
du_'8802''45'nonZero_126 Integer
v0
du_'8802''45'nonZero_126 :: Integer -> T_NonZero_112
du_'8802''45'nonZero_126 :: Integer -> T_NonZero_112
du_'8802''45'nonZero_126 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
_ -> (Any -> T_NonZero_112) -> Any -> T_NonZero_112
forall a b. a -> b
coe
             Any -> T_NonZero_112
C_NonZero'46'constructor_3575
             (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
-- Data.Nat.Base.>-nonZero
d_'62''45'nonZero_136 :: Integer -> T__'8804'__22 -> T_NonZero_112
d_'62''45'nonZero_136 :: Integer -> T__'8804'__22 -> T_NonZero_112
d_'62''45'nonZero_136 ~Integer
v0 T__'8804'__22
v1 = T__'8804'__22 -> T_NonZero_112
du_'62''45'nonZero_136 T__'8804'__22
v1
du_'62''45'nonZero_136 :: T__'8804'__22 -> T_NonZero_112
du_'62''45'nonZero_136 :: T__'8804'__22 -> T_NonZero_112
du_'62''45'nonZero_136 T__'8804'__22
v0
  = case T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22
v0 of
      C_s'8804's_34 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
C_NonZero'46'constructor_3575
                (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))
      T__'8804'__22
_ -> T_NonZero_112
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Base.≢-nonZero⁻¹
d_'8802''45'nonZero'8315''185'_140 ::
  Integer ->
  T_NonZero_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'8802''45'nonZero'8315''185'_140 :: Integer -> T_NonZero_112 -> T__'8801'__12 -> T_Irrelevant_20
d_'8802''45'nonZero'8315''185'_140 = Integer -> T_NonZero_112 -> T__'8801'__12 -> T_Irrelevant_20
forall a. a
erased
-- Data.Nat.Base.>-nonZero⁻¹
d_'62''45'nonZero'8315''185'_146 ::
  Integer -> T_NonZero_112 -> T__'8804'__22
d_'62''45'nonZero'8315''185'_146 :: Integer -> T_NonZero_112 -> T__'8804'__22
d_'62''45'nonZero'8315''185'_146 ~Integer
v0 ~T_NonZero_112
v1
  = T__'8804'__22
du_'62''45'nonZero'8315''185'_146
du_'62''45'nonZero'8315''185'_146 :: T__'8804'__22
du_'62''45'nonZero'8315''185'_146 :: T__'8804'__22
du_'62''45'nonZero'8315''185'_146
  = (T__'8804'__22 -> T__'8804'__22) -> Any -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22 -> T__'8804'__22
C_s'8804's_34 (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
C_z'8804'n_26)
-- Data.Nat.Base.NonTrivial
d_NonTrivial_152 :: p -> ()
d_NonTrivial_152 p
a0 = ()
newtype T_NonTrivial_152 = C_NonTrivial'46'constructor_5661 AgdaAny
-- Data.Nat.Base.NonTrivial.nonTrivial
d_nonTrivial_158 :: T_NonTrivial_152 -> AgdaAny
d_nonTrivial_158 :: T_NonTrivial_152 -> Any
d_nonTrivial_158 T_NonTrivial_152
v0
  = case T_NonTrivial_152 -> T_NonTrivial_152
forall a b. a -> b
coe T_NonTrivial_152
v0 of
      C_NonTrivial'46'constructor_5661 Any
v1 -> Any -> Any
forall a b. a -> b
coe Any
v1
      T_NonTrivial_152
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Base.nonTrivial
d_nonTrivial_162 :: Integer -> T_NonTrivial_152
d_nonTrivial_162 :: Integer -> T_NonTrivial_152
d_nonTrivial_162 ~Integer
v0 = T_NonTrivial_152
du_nonTrivial_162
du_nonTrivial_162 :: T_NonTrivial_152
du_nonTrivial_162 :: T_NonTrivial_152
du_nonTrivial_162
  = (Any -> T_NonTrivial_152) -> Any -> T_NonTrivial_152
forall a b. a -> b
coe
      Any -> T_NonTrivial_152
C_NonTrivial'46'constructor_5661
      (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
-- Data.Nat.Base.n>1⇒nonTrivial
d_n'62'1'8658'nonTrivial_166 ::
  Integer -> T__'8804'__22 -> T_NonTrivial_152
d_n'62'1'8658'nonTrivial_166 :: Integer -> T__'8804'__22 -> T_NonTrivial_152
d_n'62'1'8658'nonTrivial_166 ~Integer
v0 T__'8804'__22
v1
  = T__'8804'__22 -> T_NonTrivial_152
du_n'62'1'8658'nonTrivial_166 T__'8804'__22
v1
du_n'62'1'8658'nonTrivial_166 :: T__'8804'__22 -> T_NonTrivial_152
du_n'62'1'8658'nonTrivial_166 :: T__'8804'__22 -> T_NonTrivial_152
du_n'62'1'8658'nonTrivial_166 T__'8804'__22
v0
  = case T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22
v0 of
      C_s'8804's_34 T__'8804'__22
v3
        -> case T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22
v3 of
             C_s'8804's_34 T__'8804'__22
v6
               -> (Any -> Any -> Any) -> Any -> Any -> T_NonTrivial_152
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
v6)
                    ((Any -> T_NonTrivial_152) -> Any -> Any
forall a b. a -> b
coe
                       Any -> T_NonTrivial_152
C_NonTrivial'46'constructor_5661
                       (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))
             T__'8804'__22
_ -> T_NonTrivial_152
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8804'__22
_ -> T_NonTrivial_152
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Base.nonTrivial⇒nonZero
d_nonTrivial'8658'nonZero_170 ::
  Integer -> T_NonTrivial_152 -> T_NonZero_112
d_nonTrivial'8658'nonZero_170 :: Integer -> T_NonTrivial_152 -> T_NonZero_112
d_nonTrivial'8658'nonZero_170 ~Integer
v0 ~T_NonTrivial_152
v1
  = T_NonZero_112
du_nonTrivial'8658'nonZero_170
du_nonTrivial'8658'nonZero_170 :: T_NonZero_112
du_nonTrivial'8658'nonZero_170 :: T_NonZero_112
du_nonTrivial'8658'nonZero_170
  = (Any -> T_NonZero_112) -> Any -> T_NonZero_112
forall a b. a -> b
coe
      Any -> T_NonZero_112
C_NonZero'46'constructor_3575
      (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
-- Data.Nat.Base.nonTrivial⇒n>1
d_nonTrivial'8658'n'62'1_174 ::
  Integer -> T_NonTrivial_152 -> T__'8804'__22
d_nonTrivial'8658'n'62'1_174 :: Integer -> T_NonTrivial_152 -> T__'8804'__22
d_nonTrivial'8658'n'62'1_174 ~Integer
v0 ~T_NonTrivial_152
v1
  = T__'8804'__22
du_nonTrivial'8658'n'62'1_174
du_nonTrivial'8658'n'62'1_174 :: T__'8804'__22
du_nonTrivial'8658'n'62'1_174 :: T__'8804'__22
du_nonTrivial'8658'n'62'1_174
  = (T__'8804'__22 -> T__'8804'__22) -> Any -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22 -> T__'8804'__22
C_s'8804's_34 ((T__'8804'__22 -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe T__'8804'__22 -> T__'8804'__22
C_s'8804's_34 (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
C_z'8804'n_26))
-- Data.Nat.Base.nonTrivial⇒≢1
d_nonTrivial'8658''8802'1_178 ::
  Integer ->
  T_NonTrivial_152 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_nonTrivial'8658''8802'1_178 :: Integer -> T_NonTrivial_152 -> T__'8801'__12 -> T_Irrelevant_20
d_nonTrivial'8658''8802'1_178 = Integer -> T_NonTrivial_152 -> T__'8801'__12 -> T_Irrelevant_20
forall a. a
erased
-- Data.Nat.Base.+-rawMagma
d_'43''45'rawMagma_180 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawMagma_36
d_'43''45'rawMagma_180 :: T_RawMagma_36
d_'43''45'rawMagma_180
  = ((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
addInt
-- Data.Nat.Base.+-0-rawMonoid
d_'43''45'0'45'rawMonoid_182 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawMonoid_64
d_'43''45'0'45'rawMonoid_182 :: T_RawMonoid_64
d_'43''45'0'45'rawMonoid_182
  = ((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
addInt (Integer
0 :: Integer)
-- Data.Nat.Base.*-rawMagma
d_'42''45'rawMagma_184 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawMagma_36
d_'42''45'rawMagma_184 :: T_RawMagma_36
d_'42''45'rawMagma_184
  = ((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
mulInt
-- Data.Nat.Base.*-1-rawMonoid
d_'42''45'1'45'rawMonoid_186 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawMonoid_64
d_'42''45'1'45'rawMonoid_186 :: T_RawMonoid_64
d_'42''45'1'45'rawMonoid_186
  = ((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
mulInt (Integer
1 :: Integer)
-- Data.Nat.Base.+-*-rawNearSemiring
d_'43''45''42''45'rawNearSemiring_188 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawNearSemiring_134
d_'43''45''42''45'rawNearSemiring_188 :: T_RawNearSemiring_134
d_'43''45''42''45'rawNearSemiring_188
  = ((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
addInt Integer -> Integer -> Integer
mulInt (Integer
0 :: Integer)
-- Data.Nat.Base.+-*-rawSemiring
d_'43''45''42''45'rawSemiring_190 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawSemiring_174
d_'43''45''42''45'rawSemiring_190 :: T_RawSemiring_174
d_'43''45''42''45'rawSemiring_190
  = ((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
addInt Integer -> Integer -> Integer
mulInt (Integer
0 :: Integer) (Integer
1 :: Integer)
-- Data.Nat.Base.pred
d_pred_192 :: Integer -> Integer
d_pred_192 :: Integer -> Integer
d_pred_192 Integer
v0
  = (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22 Integer
v0 (Integer
1 :: Integer)
-- Data.Nat.Base._+⋎_
d__'43''8910'__196 :: Integer -> Integer -> Integer
d__'43''8910'__196 :: Integer -> Integer -> Integer
d__'43''8910'__196 Integer
v0 Integer
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> Integer -> Integer
forall a b. a -> b
coe Integer
v1
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (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
addInt (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
d__'43''8910'__196 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
-- Data.Nat.Base._⊔_
d__'8852'__204 :: Integer -> Integer -> Integer
d__'8852'__204 :: Integer -> Integer -> Integer
d__'8852'__204 Integer
v0 Integer
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> Integer -> Integer
forall a b. a -> b
coe Integer
v1
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> Integer
forall a b. a -> b
coe
             (case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
                Integer
0 -> Integer -> Any
forall a b. a -> b
coe Integer
v0
                Integer
_ -> let v3 :: Integer
v3 = 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 -> Any
forall a b. a -> b
coe
                       ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                          Integer -> Integer -> Integer
addInt (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
d__'8852'__204 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3))))
-- Data.Nat.Base._⊔′_
d__'8852''8242'__214 :: Integer -> Integer -> Integer
d__'8852''8242'__214 :: Integer -> Integer -> Integer
d__'8852''8242'__214 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 -> Any
forall a b. a -> b
coe Integer
v1 else Integer -> Any
forall a b. a -> b
coe Integer
v0)
-- Data.Nat.Base._⊓_
d__'8851'__232 :: Integer -> Integer -> Integer
d__'8851'__232 :: Integer -> Integer -> Integer
d__'8851'__232 Integer
v0 Integer
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> Integer
forall a b. a -> b
coe
             (case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
                Integer
0 -> Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)
                Integer
_ -> let v3 :: Integer
v3 = 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 -> Any
forall a b. a -> b
coe
                       ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                          Integer -> Integer -> Integer
addInt (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
d__'8851'__232 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3))))
-- Data.Nat.Base._⊓′_
d__'8851''8242'__242 :: Integer -> Integer -> Integer
d__'8851''8242'__242 :: Integer -> Integer -> Integer
d__'8851''8242'__242 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 -> Any
forall a b. a -> b
coe Integer
v0 else Integer -> Any
forall a b. a -> b
coe Integer
v1)
-- Data.Nat.Base.parity
d_parity_260 :: Integer -> MAlonzo.Code.Data.Parity.Base.T_Parity_6
d_parity_260 :: Integer -> T_Parity_6
d_parity_260 Integer
v0
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> T_Parity_6 -> T_Parity_6
forall a b. a -> b
coe T_Parity_6
MAlonzo.Code.Data.Parity.Base.C_0ℙ_8
      Integer
1 -> T_Parity_6 -> T_Parity_6
forall a b. a -> b
coe T_Parity_6
MAlonzo.Code.Data.Parity.Base.C_1ℙ_10
      Integer
_ -> let v1 :: Integer
v1 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) in
           Any -> T_Parity_6
forall a b. a -> b
coe ((Integer -> T_Parity_6) -> Any -> Any
forall a b. a -> b
coe Integer -> T_Parity_6
d_parity_260 (Integer -> Any
forall a b. a -> b
coe Integer
v1))
-- Data.Nat.Base.⌊_/2⌋
d_'8970'_'47'2'8971'_264 :: Integer -> Integer
d_'8970'_'47'2'8971'_264 :: Integer -> Integer
d_'8970'_'47'2'8971'_264 Integer
v0
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
      Integer
1 -> Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
      Integer
_ -> let v1 :: Integer
v1 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: 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
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
                ((Integer -> Integer) -> Any -> Any
forall a b. a -> b
coe Integer -> Integer
d_'8970'_'47'2'8971'_264 (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
-- Data.Nat.Base.⌈_/2⌉
d_'8968'_'47'2'8969'_268 :: Integer -> Integer
d_'8968'_'47'2'8969'_268 :: Integer -> Integer
d_'8968'_'47'2'8969'_268 Integer
v0
  = (Integer -> Integer) -> Any -> Integer
forall a b. a -> b
coe
      Integer -> Integer
d_'8970'_'47'2'8971'_264 ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
-- Data.Nat.Base._^_
d__'94'__272 :: Integer -> Integer -> Integer
d__'94'__272 :: Integer -> Integer -> Integer
d__'94'__272 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
1 :: Integer)
      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
mulInt (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'__272 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
-- Data.Nat.Base.∣_-_∣
d_'8739'_'45'_'8739'_280 :: Integer -> Integer -> Integer
d_'8739'_'45'_'8739'_280 :: Integer -> Integer -> Integer
d_'8739'_'45'_'8739'_280 Integer
v0 Integer
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> Integer -> Integer
forall a b. a -> b
coe Integer
v1
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> Integer
forall a b. a -> b
coe
             (case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
                Integer
0 -> Integer -> Any
forall a b. a -> b
coe Integer
v0
                Integer
_ -> let v3 :: Integer
v3 = 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 -> Any
forall a b. a -> b
coe ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
d_'8739'_'45'_'8739'_280 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3)))
-- Data.Nat.Base.∣_-_∣′
d_'8739'_'45'_'8739''8242'_290 :: Integer -> Integer -> Integer
d_'8739'_'45'_'8739''8242'_290 :: Integer -> Integer -> Integer
d_'8739'_'45'_'8739''8242'_290 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 -> 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.Nat.Base._/_
d__'47'__314 :: Integer -> Integer -> T_NonZero_112 -> Integer
d__'47'__314 :: Integer -> Integer -> T_NonZero_112 -> Integer
d__'47'__314 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> Integer
du__'47'__314 Integer
v0 Integer
v1
du__'47'__314 :: Integer -> Integer -> Integer
du__'47'__314 :: Integer -> Integer -> Integer
du__'47'__314 Integer
v0 Integer
v1 = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
quotInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
-- Data.Nat.Base._%_
d__'37'__326 :: Integer -> Integer -> T_NonZero_112 -> Integer
d__'37'__326 :: Integer -> Integer -> T_NonZero_112 -> Integer
d__'37'__326 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> Integer
du__'37'__326 Integer
v0 Integer
v1
du__'37'__326 :: Integer -> Integer -> Integer
du__'37'__326 :: Integer -> Integer -> Integer
du__'37'__326 Integer
v0 Integer
v1 = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
remInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
-- Data.Nat.Base._!
d__'33'_332 :: Integer -> Integer
d__'33'_332 :: Integer -> Integer
d__'33'_332 Integer
v0
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)
      Integer
_ -> let v1 :: Integer
v1 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (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
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) ((Integer -> Integer) -> Any -> Any
forall a b. a -> b
coe Integer -> Integer
d__'33'_332 (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
-- Data.Nat.Base._≤′_
d__'8804''8242'__338 :: p -> p -> ()
d__'8804''8242'__338 p
a0 p
a1 = ()
data T__'8804''8242'__338
  = C_'8804''8242''45'refl_342 |
    C_'8804''8242''45'step_348 T__'8804''8242'__338
-- Data.Nat.Base._<′_
d__'60''8242'__350 :: Integer -> Integer -> ()
d__'60''8242'__350 :: Integer -> Integer -> ()
d__'60''8242'__350 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._≥′_
d__'8805''8242'__364 :: Integer -> Integer -> ()
d__'8805''8242'__364 :: Integer -> Integer -> ()
d__'8805''8242'__364 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._>′_
d__'62''8242'__370 :: Integer -> Integer -> ()
d__'62''8242'__370 :: Integer -> Integer -> ()
d__'62''8242'__370 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._≤″_
d__'8804''8243'__380 :: Integer -> Integer -> ()
d__'8804''8243'__380 :: Integer -> Integer -> ()
d__'8804''8243'__380 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._<″_
d__'60''8243'__382 :: Integer -> Integer -> ()
d__'60''8243'__382 :: Integer -> Integer -> ()
d__'60''8243'__382 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._≥″_
d__'8805''8243'__388 :: Integer -> Integer -> ()
d__'8805''8243'__388 :: Integer -> Integer -> ()
d__'8805''8243'__388 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._>″_
d__'62''8243'__394 :: Integer -> Integer -> ()
d__'62''8243'__394 :: Integer -> Integer -> ()
d__'62''8243'__394 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base.s<″s⁻¹
d_s'60''8243's'8315''185'_404 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Algebra.Definitions.RawMagma.T__'8739''737'__26 ->
  MAlonzo.Code.Algebra.Definitions.RawMagma.T__'8739''737'__26
d_s'60''8243's'8315''185'_404 :: Integer -> Integer -> T__'8739''737'__26 -> T__'8739''737'__26
d_s'60''8243's'8315''185'_404 ~Integer
v0 ~Integer
v1 T__'8739''737'__26
v2
  = T__'8739''737'__26 -> T__'8739''737'__26
du_s'60''8243's'8315''185'_404 T__'8739''737'__26
v2
du_s'60''8243's'8315''185'_404 ::
  MAlonzo.Code.Algebra.Definitions.RawMagma.T__'8739''737'__26 ->
  MAlonzo.Code.Algebra.Definitions.RawMagma.T__'8739''737'__26
du_s'60''8243's'8315''185'_404 :: T__'8739''737'__26 -> T__'8739''737'__26
du_s'60''8243's'8315''185'_404 T__'8739''737'__26
v0 = T__'8739''737'__26 -> T__'8739''737'__26
forall a b. a -> b
coe T__'8739''737'__26
v0
-- Data.Nat.Base._≤‴_
d__'8804''8244'__408 :: p -> p -> ()
d__'8804''8244'__408 p
a0 p
a1 = ()
data T__'8804''8244'__408
  = C_'8804''8244''45'refl_412 |
    C_'8804''8244''45'step_418 T__'8804''8244'__408
-- Data.Nat.Base._<‴_
d__'60''8244'__420 :: Integer -> Integer -> ()
d__'60''8244'__420 :: Integer -> Integer -> ()
d__'60''8244'__420 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._≥‴_
d__'8805''8244'__426 :: Integer -> Integer -> ()
d__'8805''8244'__426 :: Integer -> Integer -> ()
d__'8805''8244'__426 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._>‴_
d__'62''8244'__432 :: Integer -> Integer -> ()
d__'62''8244'__432 :: Integer -> Integer -> ()
d__'62''8244'__432 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base.Ordering
d_Ordering_438 :: p -> p -> ()
d_Ordering_438 p
a0 p
a1 = ()
data T_Ordering_438
  = C_less_444 Integer | C_equal_448 | C_greater_454 Integer
-- Data.Nat.Base.compare
d_compare_460 :: Integer -> Integer -> T_Ordering_438
d_compare_460 :: Integer -> Integer -> T_Ordering_438
d_compare_460 Integer
v0 Integer
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
             Integer
0 -> T_Ordering_438 -> T_Ordering_438
forall a b. a -> b
coe T_Ordering_438
C_equal_448
             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 -> T_Ordering_438
forall a b. a -> b
coe ((Integer -> T_Ordering_438) -> Integer -> Any
forall a b. a -> b
coe Integer -> T_Ordering_438
C_less_444 Integer
v2)
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> T_Ordering_438
forall a b. a -> b
coe
             (case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
                Integer
0 -> (Integer -> T_Ordering_438) -> Integer -> Any
forall a b. a -> b
coe Integer -> T_Ordering_438
C_greater_454 Integer
v2
                Integer
_ -> let v3 :: Integer
v3 = 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 -> Any
forall a b. a -> b
coe ((Integer -> Integer -> T_Ordering_438) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> T_Ordering_438
d_compare_460 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3)))
-- Data.Nat.Base.s≤″s⁻¹
d_s'8804''8243's'8315''185'_514 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Algebra.Definitions.RawMagma.T__'8739''737'__26 ->
  MAlonzo.Code.Algebra.Definitions.RawMagma.T__'8739''737'__26
d_s'8804''8243's'8315''185'_514 :: Integer -> Integer -> T__'8739''737'__26 -> T__'8739''737'__26
d_s'8804''8243's'8315''185'_514 ~Integer
v0 ~Integer
v1 T__'8739''737'__26
v2
  = T__'8739''737'__26 -> T__'8739''737'__26
du_s'8804''8243's'8315''185'_514 T__'8739''737'__26
v2
du_s'8804''8243's'8315''185'_514 ::
  MAlonzo.Code.Algebra.Definitions.RawMagma.T__'8739''737'__26 ->
  MAlonzo.Code.Algebra.Definitions.RawMagma.T__'8739''737'__26
du_s'8804''8243's'8315''185'_514 :: T__'8739''737'__26 -> T__'8739''737'__26
du_s'8804''8243's'8315''185'_514 T__'8739''737'__26
v0 = T__'8739''737'__26 -> T__'8739''737'__26
forall a b. a -> b
coe T__'8739''737'__26
v0