{-# 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_constructor_120 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_constructor_120 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_124 :: Integer -> T_NonZero_112
d_nonZero_124 :: Integer -> T_NonZero_112
d_nonZero_124 ~Integer
v0 = T_NonZero_112
du_nonZero_124
du_nonZero_124 :: T_NonZero_112
du_nonZero_124 :: T_NonZero_112
du_nonZero_124
  = (Any -> T_NonZero_112) -> Any -> T_NonZero_112
forall a b. a -> b
coe Any -> T_NonZero_112
C_constructor_120 (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
-- Data.Nat.Base.≢-nonZero
d_'8802''45'nonZero_128 ::
  Integer ->
  (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  T_NonZero_112
d_'8802''45'nonZero_128 :: Integer -> (T__'8801'__12 -> T_Irrelevant_20) -> T_NonZero_112
d_'8802''45'nonZero_128 Integer
v0 ~T__'8801'__12 -> T_Irrelevant_20
v1 = Integer -> T_NonZero_112
du_'8802''45'nonZero_128 Integer
v0
du_'8802''45'nonZero_128 :: Integer -> T_NonZero_112
du_'8802''45'nonZero_128 :: Integer -> T_NonZero_112
du_'8802''45'nonZero_128 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_constructor_120 (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
-- Data.Nat.Base.>-nonZero
d_'62''45'nonZero_138 :: Integer -> T__'8804'__22 -> T_NonZero_112
d_'62''45'nonZero_138 :: Integer -> T__'8804'__22 -> T_NonZero_112
d_'62''45'nonZero_138 ~Integer
v0 T__'8804'__22
v1 = T__'8804'__22 -> T_NonZero_112
du_'62''45'nonZero_138 T__'8804'__22
v1
du_'62''45'nonZero_138 :: T__'8804'__22 -> T_NonZero_112
du_'62''45'nonZero_138 :: T__'8804'__22 -> T_NonZero_112
du_'62''45'nonZero_138 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_constructor_120 (() -> 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'_142 ::
  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'_142 :: Integer -> T_NonZero_112 -> T__'8801'__12 -> T_Irrelevant_20
d_'8802''45'nonZero'8315''185'_142 = Integer -> T_NonZero_112 -> T__'8801'__12 -> T_Irrelevant_20
forall a. a
erased
-- Data.Nat.Base.>-nonZero⁻¹
d_'62''45'nonZero'8315''185'_148 ::
  Integer -> T_NonZero_112 -> T__'8804'__22
d_'62''45'nonZero'8315''185'_148 :: Integer -> T_NonZero_112 -> T__'8804'__22
d_'62''45'nonZero'8315''185'_148 ~Integer
v0 ~T_NonZero_112
v1
  = T__'8804'__22
du_'62''45'nonZero'8315''185'_148
du_'62''45'nonZero'8315''185'_148 :: T__'8804'__22
du_'62''45'nonZero'8315''185'_148 :: T__'8804'__22
du_'62''45'nonZero'8315''185'_148
  = (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_154 :: p -> ()
d_NonTrivial_154 p
a0 = ()
newtype T_NonTrivial_154 = C_constructor_162 AgdaAny
-- Data.Nat.Base.NonTrivial.nonTrivial
d_nonTrivial_160 :: T_NonTrivial_154 -> AgdaAny
d_nonTrivial_160 :: T_NonTrivial_154 -> Any
d_nonTrivial_160 T_NonTrivial_154
v0
  = case T_NonTrivial_154 -> T_NonTrivial_154
forall a b. a -> b
coe T_NonTrivial_154
v0 of
      C_constructor_162 Any
v1 -> Any -> Any
forall a b. a -> b
coe Any
v1
      T_NonTrivial_154
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Base.nonTrivial
d_nonTrivial_166 :: Integer -> T_NonTrivial_154
d_nonTrivial_166 :: Integer -> T_NonTrivial_154
d_nonTrivial_166 ~Integer
v0 = T_NonTrivial_154
du_nonTrivial_166
du_nonTrivial_166 :: T_NonTrivial_154
du_nonTrivial_166 :: T_NonTrivial_154
du_nonTrivial_166
  = (Any -> T_NonTrivial_154) -> Any -> T_NonTrivial_154
forall a b. a -> b
coe Any -> T_NonTrivial_154
C_constructor_162 (() -> 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_170 ::
  Integer -> T__'8804'__22 -> T_NonTrivial_154
d_n'62'1'8658'nonTrivial_170 :: Integer -> T__'8804'__22 -> T_NonTrivial_154
d_n'62'1'8658'nonTrivial_170 ~Integer
v0 T__'8804'__22
v1
  = T__'8804'__22 -> T_NonTrivial_154
du_n'62'1'8658'nonTrivial_170 T__'8804'__22
v1
du_n'62'1'8658'nonTrivial_170 :: T__'8804'__22 -> T_NonTrivial_154
du_n'62'1'8658'nonTrivial_170 :: T__'8804'__22 -> T_NonTrivial_154
du_n'62'1'8658'nonTrivial_170 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_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
v6)
                    ((Any -> T_NonTrivial_154) -> Any -> Any
forall a b. a -> b
coe Any -> T_NonTrivial_154
C_constructor_162 (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))
             T__'8804'__22
_ -> T_NonTrivial_154
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8804'__22
_ -> T_NonTrivial_154
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Base.nonTrivial⇒nonZero
d_nonTrivial'8658'nonZero_174 ::
  Integer -> T_NonTrivial_154 -> T_NonZero_112
d_nonTrivial'8658'nonZero_174 :: Integer -> T_NonTrivial_154 -> T_NonZero_112
d_nonTrivial'8658'nonZero_174 ~Integer
v0 ~T_NonTrivial_154
v1
  = T_NonZero_112
du_nonTrivial'8658'nonZero_174
du_nonTrivial'8658'nonZero_174 :: T_NonZero_112
du_nonTrivial'8658'nonZero_174 :: T_NonZero_112
du_nonTrivial'8658'nonZero_174
  = (Any -> T_NonZero_112) -> Any -> T_NonZero_112
forall a b. a -> b
coe Any -> T_NonZero_112
C_constructor_120 (() -> 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_178 ::
  Integer -> T_NonTrivial_154 -> T__'8804'__22
d_nonTrivial'8658'n'62'1_178 :: Integer -> T_NonTrivial_154 -> T__'8804'__22
d_nonTrivial'8658'n'62'1_178 ~Integer
v0 ~T_NonTrivial_154
v1
  = T__'8804'__22
du_nonTrivial'8658'n'62'1_178
du_nonTrivial'8658'n'62'1_178 :: T__'8804'__22
du_nonTrivial'8658'n'62'1_178 :: T__'8804'__22
du_nonTrivial'8658'n'62'1_178
  = (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_182 ::
  Integer ->
  T_NonTrivial_154 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_nonTrivial'8658''8802'1_182 :: Integer -> T_NonTrivial_154 -> T__'8801'__12 -> T_Irrelevant_20
d_nonTrivial'8658''8802'1_182 = Integer -> T_NonTrivial_154 -> T__'8801'__12 -> T_Irrelevant_20
forall a. a
erased
-- Data.Nat.Base.+-rawMagma
d_'43''45'rawMagma_184 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawMagma_44
d_'43''45'rawMagma_184 :: T_RawMagma_44
d_'43''45'rawMagma_184
  = ((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
addInt
-- Data.Nat.Base.+-0-rawMonoid
d_'43''45'0'45'rawMonoid_186 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawMonoid_74
d_'43''45'0'45'rawMonoid_186 :: T_RawMonoid_74
d_'43''45'0'45'rawMonoid_186
  = ((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
addInt
      (Integer
0 :: Integer)
-- Data.Nat.Base.*-rawMagma
d_'42''45'rawMagma_188 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawMagma_44
d_'42''45'rawMagma_188 :: T_RawMagma_44
d_'42''45'rawMagma_188
  = ((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
mulInt
-- Data.Nat.Base.*-1-rawMonoid
d_'42''45'1'45'rawMonoid_190 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawMonoid_74
d_'42''45'1'45'rawMonoid_190 :: T_RawMonoid_74
d_'42''45'1'45'rawMonoid_190
  = ((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
mulInt
      (Integer
1 :: Integer)
-- Data.Nat.Base.+-*-rawNearSemiring
d_'43''45''42''45'rawNearSemiring_192 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawNearSemiring_148
d_'43''45''42''45'rawNearSemiring_192 :: T_RawNearSemiring_148
d_'43''45''42''45'rawNearSemiring_192
  = ((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
addInt Integer -> Integer -> Integer
mulInt
      (Integer
0 :: Integer)
-- Data.Nat.Base.+-*-rawSemiring
d_'43''45''42''45'rawSemiring_194 ::
  MAlonzo.Code.Algebra.Bundles.Raw.T_RawSemiring_190
d_'43''45''42''45'rawSemiring_194 :: T_RawSemiring_190
d_'43''45''42''45'rawSemiring_194
  = ((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
addInt Integer -> Integer -> Integer
mulInt
      (Integer
0 :: Integer) (Integer
1 :: Integer)
-- Data.Nat.Base.pred
d_pred_196 :: Integer -> Integer
d_pred_196 :: Integer -> Integer
d_pred_196 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'__200 :: Integer -> Integer -> Integer
d__'43''8910'__200 :: Integer -> Integer -> Integer
d__'43''8910'__200 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'__200 (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'__208 :: Integer -> Integer -> Integer
d__'8852'__208 :: Integer -> Integer -> Integer
d__'8852'__208 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'__208 (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'__218 :: Integer -> Integer -> Integer
d__'8852''8242'__218 :: Integer -> Integer -> Integer
d__'8852''8242'__218 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'__236 :: Integer -> Integer -> Integer
d__'8851'__236 :: Integer -> Integer -> Integer
d__'8851'__236 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'__236 (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'__246 :: Integer -> Integer -> Integer
d__'8851''8242'__246 :: Integer -> Integer -> Integer
d__'8851''8242'__246 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_264 :: Integer -> MAlonzo.Code.Data.Parity.Base.T_Parity_6
d_parity_264 :: Integer -> T_Parity_6
d_parity_264 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_264 (Integer -> Any
forall a b. a -> b
coe Integer
v1))
-- Data.Nat.Base.⌊_/2⌋
d_'8970'_'47'2'8971'_268 :: Integer -> Integer
d_'8970'_'47'2'8971'_268 :: Integer -> Integer
d_'8970'_'47'2'8971'_268 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'_268 (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
-- Data.Nat.Base.⌈_/2⌉
d_'8968'_'47'2'8969'_272 :: Integer -> Integer
d_'8968'_'47'2'8969'_272 :: Integer -> Integer
d_'8968'_'47'2'8969'_272 Integer
v0
  = (Integer -> Integer) -> Any -> Integer
forall a b. a -> b
coe
      Integer -> Integer
d_'8970'_'47'2'8971'_268 ((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'__276 :: Integer -> Integer -> Integer
d__'94'__276 :: Integer -> Integer -> Integer
d__'94'__276 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'__276 (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'_284 :: Integer -> Integer -> Integer
d_'8739'_'45'_'8739'_284 :: Integer -> Integer -> Integer
d_'8739'_'45'_'8739'_284 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'_284 (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'_294 :: Integer -> Integer -> Integer
d_'8739'_'45'_'8739''8242'_294 :: Integer -> Integer -> Integer
d_'8739'_'45'_'8739''8242'_294 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'__318 :: Integer -> Integer -> T_NonZero_112 -> Integer
d__'47'__318 :: Integer -> Integer -> T_NonZero_112 -> Integer
d__'47'__318 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> Integer
du__'47'__318 Integer
v0 Integer
v1
du__'47'__318 :: Integer -> Integer -> Integer
du__'47'__318 :: Integer -> Integer -> Integer
du__'47'__318 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'__330 :: Integer -> Integer -> T_NonZero_112 -> Integer
d__'37'__330 :: Integer -> Integer -> T_NonZero_112 -> Integer
d__'37'__330 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> Integer
du__'37'__330 Integer
v0 Integer
v1
du__'37'__330 :: Integer -> Integer -> Integer
du__'37'__330 :: Integer -> Integer -> Integer
du__'37'__330 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'_336 :: Integer -> Integer
d__'33'_336 :: Integer -> Integer
d__'33'_336 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'_336 (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
-- Data.Nat.Base._≤′_
d__'8804''8242'__342 :: p -> p -> ()
d__'8804''8242'__342 p
a0 p
a1 = ()
data T__'8804''8242'__342
  = C_'8804''8242''45'reflexive_348 |
    C_'8804''8242''45'step_352 T__'8804''8242'__342
-- Data.Nat.Base._<′_
d__'60''8242'__358 :: Integer -> Integer -> ()
d__'60''8242'__358 :: Integer -> Integer -> ()
d__'60''8242'__358 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._≥′_
d__'8805''8242'__372 :: Integer -> Integer -> ()
d__'8805''8242'__372 :: Integer -> Integer -> ()
d__'8805''8242'__372 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._>′_
d__'62''8242'__378 :: Integer -> Integer -> ()
d__'62''8242'__378 :: Integer -> Integer -> ()
d__'62''8242'__378 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._≤″_
d__'8804''8243'__388 :: Integer -> Integer -> ()
d__'8804''8243'__388 :: Integer -> Integer -> ()
d__'8804''8243'__388 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._<″_
d__'60''8243'__390 :: Integer -> Integer -> ()
d__'60''8243'__390 :: Integer -> Integer -> ()
d__'60''8243'__390 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._≥″_
d__'8805''8243'__396 :: Integer -> Integer -> ()
d__'8805''8243'__396 :: Integer -> Integer -> ()
d__'8805''8243'__396 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._>″_
d__'62''8243'__402 :: Integer -> Integer -> ()
d__'62''8243'__402 :: Integer -> Integer -> ()
d__'62''8243'__402 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base.s<″s⁻¹
d_s'60''8243's'8315''185'_412 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Algebra.Definitions.RawMagma.T__'8739''737'__28 ->
  MAlonzo.Code.Algebra.Definitions.RawMagma.T__'8739''737'__28
d_s'60''8243's'8315''185'_412 :: Integer -> Integer -> T__'8739''737'__28 -> T__'8739''737'__28
d_s'60''8243's'8315''185'_412 ~Integer
v0 ~Integer
v1 T__'8739''737'__28
v2
  = T__'8739''737'__28 -> T__'8739''737'__28
du_s'60''8243's'8315''185'_412 T__'8739''737'__28
v2
du_s'60''8243's'8315''185'_412 ::
  MAlonzo.Code.Algebra.Definitions.RawMagma.T__'8739''737'__28 ->
  MAlonzo.Code.Algebra.Definitions.RawMagma.T__'8739''737'__28
du_s'60''8243's'8315''185'_412 :: T__'8739''737'__28 -> T__'8739''737'__28
du_s'60''8243's'8315''185'_412 T__'8739''737'__28
v0 = T__'8739''737'__28 -> T__'8739''737'__28
forall a b. a -> b
coe T__'8739''737'__28
v0
-- Data.Nat.Base._≤‴_
d__'8804''8244'__422 :: p -> p -> ()
d__'8804''8244'__422 p
a0 p
a1 = ()
data T__'8804''8244'__422
  = C_'8804''8244''45'reflexive_434 |
    C_'8804''8244''45'step_436 T__'8804''8244'__422
-- Data.Nat.Base._<‴_
d__'60''8244'__424 :: Integer -> Integer -> ()
d__'60''8244'__424 :: Integer -> Integer -> ()
d__'60''8244'__424 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._≥‴_
d__'8805''8244'__440 :: Integer -> Integer -> ()
d__'8805''8244'__440 :: Integer -> Integer -> ()
d__'8805''8244'__440 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._>‴_
d__'62''8244'__446 :: Integer -> Integer -> ()
d__'62''8244'__446 :: Integer -> Integer -> ()
d__'62''8244'__446 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base.Ordering
d_Ordering_452 :: p -> p -> ()
d_Ordering_452 p
a0 p
a1 = ()
data T_Ordering_452
  = C_less_458 Integer | C_equal_462 | C_greater_468 Integer
-- Data.Nat.Base.compare
d_compare_474 :: Integer -> Integer -> T_Ordering_452
d_compare_474 :: Integer -> Integer -> T_Ordering_452
d_compare_474 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_452 -> T_Ordering_452
forall a b. a -> b
coe T_Ordering_452
C_equal_462
             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_452
forall a b. a -> b
coe ((Integer -> T_Ordering_452) -> Integer -> Any
forall a b. a -> b
coe Integer -> T_Ordering_452
C_less_458 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_452
forall a b. a -> b
coe
             (case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
                Integer
0 -> (Integer -> T_Ordering_452) -> Integer -> Any
forall a b. a -> b
coe Integer -> T_Ordering_452
C_greater_468 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_452) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> T_Ordering_452
d_compare_474 (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'_528 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Algebra.Definitions.RawMagma.T__'8739''737'__28 ->
  MAlonzo.Code.Algebra.Definitions.RawMagma.T__'8739''737'__28
d_s'8804''8243's'8315''185'_528 :: Integer -> Integer -> T__'8739''737'__28 -> T__'8739''737'__28
d_s'8804''8243's'8315''185'_528 ~Integer
v0 ~Integer
v1 T__'8739''737'__28
v2
  = T__'8739''737'__28 -> T__'8739''737'__28
du_s'8804''8243's'8315''185'_528 T__'8739''737'__28
v2
du_s'8804''8243's'8315''185'_528 ::
  MAlonzo.Code.Algebra.Definitions.RawMagma.T__'8739''737'__28 ->
  MAlonzo.Code.Algebra.Definitions.RawMagma.T__'8739''737'__28
du_s'8804''8243's'8315''185'_528 :: T__'8739''737'__28 -> T__'8739''737'__28
du_s'8804''8243's'8315''185'_528 T__'8739''737'__28
v0 = T__'8739''737'__28 -> T__'8739''737'__28
forall a b. a -> b
coe T__'8739''737'__28
v0