{-# 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.Unit
import qualified MAlonzo.Code.Data.Empty
import qualified MAlonzo.Code.Data.Nat.Base
import qualified MAlonzo.Code.Data.Sign.Base
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'__18 |
C_'45''8804''43'_40 |
C_'43''8804''43'_48 MAlonzo.Code.Data.Nat.Base.T__'8804'__18
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'__18 |
C_'45''60''43'_64 |
C_'43''60''43'_72 MAlonzo.Code.Data.Nat.Base.T__'8804'__18
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'__10 (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'__10 (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_132 :: Integer -> ()
d_Positive_132 :: Integer -> ()
d_Positive_132 = Integer -> ()
forall a. a
erased
d_Negative_138 :: Integer -> ()
d_Negative_138 :: Integer -> ()
d_Negative_138 = Integer -> ()
forall a. a
erased
d_NonPositive_144 :: Integer -> ()
d_NonPositive_144 :: Integer -> ()
d_NonPositive_144 = Integer -> ()
forall a. a
erased
d_NonNegative_150 :: Integer -> ()
d_NonNegative_150 :: Integer -> ()
d_NonNegative_150 = Integer -> ()
forall a. a
erased
d_'8802''45'nonZero_158 ::
Integer ->
(MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4) ->
AgdaAny
d_'8802''45'nonZero_158 :: Integer -> (T__'8801'__12 -> T_'8869'_4) -> Any
d_'8802''45'nonZero_158 Integer
v0 T__'8801'__12 -> T_'8869'_4
v1
= case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
0 -> (T__'8801'__12 -> T_'8869'_4) -> Any -> Any
forall a b. a -> b
coe T__'8801'__12 -> T_'8869'_4
v1 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
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8
Integer
_ -> () -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8
d_'62''45'nonZero_168 :: Integer -> T__'60'__50 -> AgdaAny
d_'62''45'nonZero_168 :: Integer -> T__'60'__50 -> Any
d_'62''45'nonZero_168 ~Integer
v0 T__'60'__50
v1 = T__'60'__50 -> Any
du_'62''45'nonZero_168 T__'60'__50
v1
du_'62''45'nonZero_168 :: T__'60'__50 -> AgdaAny
du_'62''45'nonZero_168 :: T__'60'__50 -> Any
du_'62''45'nonZero_168 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'__18
v3
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> Any
forall a b. a -> b -> b
seq (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v3) (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
T__'60'__50
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'60''45'nonZero_174 :: Integer -> T__'60'__50 -> AgdaAny
d_'60''45'nonZero_174 :: Integer -> T__'60'__50 -> Any
d_'60''45'nonZero_174 ~Integer
v0 T__'60'__50
v1 = T__'60'__50 -> Any
du_'60''45'nonZero_174 T__'60'__50
v1
du_'60''45'nonZero_174 :: T__'60'__50 -> AgdaAny
du_'60''45'nonZero_174 :: T__'60'__50 -> Any
du_'60''45'nonZero_174 T__'60'__50
v0
= (Any -> Any -> Any) -> Any -> Any -> Any
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
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
d_positive_178 :: Integer -> T__'60'__50 -> AgdaAny
d_positive_178 :: Integer -> T__'60'__50 -> Any
d_positive_178 ~Integer
v0 T__'60'__50
v1 = T__'60'__50 -> Any
du_positive_178 T__'60'__50
v1
du_positive_178 :: T__'60'__50 -> AgdaAny
du_positive_178 :: T__'60'__50 -> Any
du_positive_178 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'__18
v3
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> Any
forall a b. a -> b -> b
seq (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v3) (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
T__'60'__50
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
d_negative_184 :: Integer -> T__'60'__50 -> AgdaAny
d_negative_184 :: Integer -> T__'60'__50 -> Any
d_negative_184 ~Integer
v0 T__'60'__50
v1 = T__'60'__50 -> Any
du_negative_184 T__'60'__50
v1
du_negative_184 :: T__'60'__50 -> AgdaAny
du_negative_184 :: T__'60'__50 -> Any
du_negative_184 T__'60'__50
v0
= (Any -> Any -> Any) -> Any -> Any -> Any
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
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
d_nonPositive_188 :: Integer -> T__'8804'__26 -> AgdaAny
d_nonPositive_188 :: Integer -> T__'8804'__26 -> Any
d_nonPositive_188 ~Integer
v0 T__'8804'__26
v1 = T__'8804'__26 -> Any
du_nonPositive_188 T__'8804'__26
v1
du_nonPositive_188 :: T__'8804'__26 -> AgdaAny
du_nonPositive_188 :: T__'8804'__26 -> Any
du_nonPositive_188 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
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8
C_'43''8804''43'_48 T__'8804'__18
v3
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> Any
forall a b. a -> b -> b
seq (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v3) (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
T__'8804'__26
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
d_nonNegative_192 :: Integer -> T__'8804'__26 -> AgdaAny
d_nonNegative_192 :: Integer -> T__'8804'__26 -> Any
d_nonNegative_192 Integer
v0 ~T__'8804'__26
v1 = Integer -> Any
du_nonNegative_192 Integer
v0
du_nonNegative_192 :: Integer -> AgdaAny
du_nonNegative_192 :: Integer -> Any
du_nonNegative_192 Integer
v0
= (Any -> Any -> Any) -> Any -> Any -> Any
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
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
d__'9667'__196 ::
MAlonzo.Code.Data.Sign.Base.T_Sign_6 -> Integer -> Integer
d__'9667'__196 :: T_Sign_6 -> Integer -> Integer
d__'9667'__196 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_202 :: p -> ()
d_SignAbs_202 p
a0 = ()
data T_SignAbs_202
= C__'9666'__208 MAlonzo.Code.Data.Sign.Base.T_Sign_6 Integer
d_signAbs_212 :: Integer -> T_SignAbs_202
d_signAbs_212 :: Integer -> T_SignAbs_202
d_signAbs_212 Integer
v0
= case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
0 -> (T_Sign_6 -> Integer -> T_SignAbs_202)
-> Any -> Any -> T_SignAbs_202
forall a b. a -> b
coe
T_Sign_6 -> Integer -> T_SignAbs_202
C__'9666'__208 (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_202)
-> Any -> Any -> T_SignAbs_202
forall a b. a -> b
coe
T_Sign_6 -> Integer -> T_SignAbs_202
C__'9666'__208 (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_202)
-> Any -> Any -> T_SignAbs_202
forall a b. a -> b
coe
T_Sign_6 -> Integer -> T_SignAbs_202
C__'9666'__208 (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'__218 :: Integer -> Integer
d_'45'__218 :: Integer -> Integer
d_'45'__218 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'__224 :: Integer -> Integer -> Integer
d__'8854'__224 :: Integer -> Integer -> Integer
d__'8854'__224 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'__218 ((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'__242 :: Integer -> Integer -> Integer
d__'43'__242 :: Integer -> Integer -> Integer
d__'43'__242 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'__224 (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'__224 (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'__260 :: Integer -> Integer -> Integer
d__'45'__260 :: Integer -> Integer -> Integer
d__'45'__260 Integer
v0 Integer
v1
= (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
d__'43'__242 (Integer -> Any
forall a b. a -> b
coe Integer
v0) ((Integer -> Integer) -> Any -> Any
forall a b. a -> b
coe Integer -> Integer
d_'45'__218 (Integer -> Any
forall a b. a -> b
coe Integer
v1))
d_suc_266 :: Integer -> Integer
d_suc_266 :: Integer -> Integer
d_suc_266 Integer
v0 = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
d__'43'__242 (Integer -> Any
forall a b. a -> b
coe Integer
d_1ℤ_16) (Integer -> Any
forall a b. a -> b
coe Integer
v0)
d_pred_270 :: Integer -> Integer
d_pred_270 :: Integer -> Integer
d_pred_270 Integer
v0 = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
d__'43'__242 (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'__274 :: Integer -> Integer -> Integer
d__'42'__274 :: Integer -> Integer -> Integer
d__'42'__274 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'__196
((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__'8852'__280 :: Integer -> Integer -> Integer
d__'8852'__280 :: Integer -> Integer -> Integer
d__'8852'__280 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'__106 (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'__116 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3))))
d__'8851'__298 :: Integer -> Integer -> Integer
d__'8851'__298 :: Integer -> Integer -> Integer
d__'8851'__298 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'__116 (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'__106 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3))))
d__'60''8242'__316 :: Integer -> Integer -> ()
d__'60''8242'__316 :: Integer -> Integer -> ()
d__'60''8242'__316 = Integer -> Integer -> ()
forall a. a
erased
d__'62''8242'__322 :: Integer -> Integer -> ()
d__'62''8242'__322 :: Integer -> Integer -> ()
d__'62''8242'__322 = Integer -> Integer -> ()
forall a. a
erased
d__'8814''8242'__328 :: Integer -> Integer -> ()
d__'8814''8242'__328 :: Integer -> Integer -> ()
d__'8814''8242'__328 = Integer -> Integer -> ()
forall a. a
erased
d__'8815''8242'__334 :: Integer -> Integer -> ()
d__'8815''8242'__334 :: Integer -> Integer -> ()
d__'8815''8242'__334 = Integer -> Integer -> ()
forall a. a
erased