{-# 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
d_0ℤ_12 :: Integer
d_0ℤ_12 :: Integer
d_0ℤ_12 = Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
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)
d_1ℤ_16 :: Integer
d_1ℤ_16 :: Integer
d_1ℤ_16 = Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)
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)
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
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
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
d__'8805'__74 :: Integer -> Integer -> ()
d__'8805'__74 :: Integer -> Integer -> ()
d__'8805'__74 = Integer -> Integer -> ()
forall a. a
erased
d__'62'__80 :: Integer -> Integer -> ()
d__'62'__80 :: Integer -> Integer -> ()
d__'62'__80 = Integer -> Integer -> ()
forall a. a
erased
d__'8816'__86 :: Integer -> Integer -> ()
d__'8816'__86 :: Integer -> Integer -> ()
d__'8816'__86 = Integer -> Integer -> ()
forall a. a
erased
d__'8817'__92 :: Integer -> Integer -> ()
d__'8817'__92 :: Integer -> Integer -> ()
d__'8817'__92 = Integer -> Integer -> ()
forall a. a
erased
d__'8814'__98 :: Integer -> Integer -> ()
d__'8814'__98 :: Integer -> Integer -> ()
d__'8814'__98 = Integer -> Integer -> ()
forall a. a
erased
d__'8815'__104 :: Integer -> Integer -> ()
d__'8815'__104 :: Integer -> Integer -> ()
d__'8815'__104 = Integer -> Integer -> ()
forall a. a
erased
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)))
d_NonZero_128 :: Integer -> ()
d_NonZero_128 :: Integer -> ()
d_NonZero_128 = Integer -> ()
forall a. a
erased
d_Positive_134 :: p -> ()
d_Positive_134 p
a0 = ()
newtype T_Positive_134 = C_Positive'46'constructor_1399 AgdaAny
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
d_NonNegative_144 :: p -> ()
d_NonNegative_144 p
a0 = ()
newtype T_NonNegative_144
= C_NonNegative'46'constructor_1457 AgdaAny
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
d_NonPositive_154 :: p -> ()
d_NonPositive_154 p
a0 = ()
newtype T_NonPositive_154
= C_NonPositive'46'constructor_1515 AgdaAny
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
d_Negative_164 :: p -> ()
d_Negative_164 p
a0 = ()
newtype T_Negative_164 = C_Negative'46'constructor_1573 AgdaAny
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
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)
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)
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)
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)
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)
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)
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
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))
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
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))
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
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))
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
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
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))
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)
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))
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)
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))
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)
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)
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)))
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)))
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))))
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))))
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)))
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)))
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)
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))
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
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
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
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
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
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
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
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