{-# 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.Digit 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.Char
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.List
import qualified MAlonzo.Code.Agda.Builtin.Nat
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Data.Fin.Base
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.Nat.Base
import qualified MAlonzo.Code.Data.Nat.DivMod
import qualified MAlonzo.Code.Data.Nat.Properties
import qualified MAlonzo.Code.Data.Vec.Base
import qualified MAlonzo.Code.Induction.WellFounded
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Syntax
d_Digit_4 :: Integer -> ()
d_Digit_4 :: Integer -> ()
d_Digit_4 = Integer -> ()
forall a. a
erased
d_Decimal_8 :: ()
d_Decimal_8 :: ()
d_Decimal_8 = ()
forall a. a
erased
d_Bit_10 :: ()
d_Bit_10 :: ()
d_Bit_10 = ()
forall a. a
erased
d_0b_12 :: MAlonzo.Code.Data.Fin.Base.T_Fin_10
d_0b_12 :: T_Fin_10
d_0b_12 = T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12
d_1b_14 :: MAlonzo.Code.Data.Fin.Base.T_Fin_10
d_1b_14 :: T_Fin_10
d_1b_14
= (T_Fin_10 -> T_Fin_10) -> Any -> T_Fin_10
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
d_toNatDigits_20 :: Integer -> AgdaAny -> Integer -> [Integer]
d_toNatDigits_20 :: Integer -> Any -> Integer -> [Integer]
d_toNatDigits_20 Integer
v0 ~Any
v1 Integer
v2 = Integer -> Integer -> [Integer]
du_toNatDigits_20 Integer
v0 Integer
v2
du_toNatDigits_20 :: Integer -> Integer -> [Integer]
du_toNatDigits_20 :: Integer -> Integer -> [Integer]
du_toNatDigits_20 Integer
v0 Integer
v1
= case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
1 -> (Integer -> Any -> [Any]) -> Any -> Any -> [Integer]
forall a b. a -> b
coe
Integer -> Any -> [Any]
MAlonzo.Code.Data.List.Base.du_replicate_294 (Integer -> Any
forall a b. a -> b
coe Integer
v1)
(Integer -> Any
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
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) in
Any -> [Integer]
forall a b. a -> b
coe
((Integer -> Integer -> [Integer] -> [Integer])
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> [Integer] -> [Integer]
du_aux_36 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
([Any] -> Any
forall a b. a -> b
coe [Any]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16))
d_aux_36 ::
Integer ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
Integer ->
Integer ->
MAlonzo.Code.Induction.WellFounded.T_Acc_42 ->
[Integer] -> [Integer]
d_aux_36 :: Integer
-> () -> Integer -> Integer -> T_Acc_42 -> [Integer] -> [Integer]
d_aux_36 Integer
v0 ~()
v1 ~Integer
v2 Integer
v3 ~T_Acc_42
v4 [Integer]
v5 = Integer -> Integer -> [Integer] -> [Integer]
du_aux_36 Integer
v0 Integer
v3 [Integer]
v5
du_aux_36 :: Integer -> Integer -> [Integer] -> [Integer]
du_aux_36 :: Integer -> Integer -> [Integer] -> [Integer]
du_aux_36 Integer
v0 Integer
v1 [Integer]
v2
= case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
Integer
0 -> (Any -> [Any] -> [Any]) -> Any -> Any -> [Integer]
forall a b. a -> b
coe
Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
([Integer] -> Any
forall a b. a -> b
coe [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 -> [Integer]
forall a b. a -> b
coe
(let v4 :: Bool
v4
= Integer -> Integer -> Bool
ltInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer))
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60 (Integer
0 :: Integer)
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v3 Integer
v0) in
Any -> Any
forall a b. a -> b
coe
(if Bool -> Bool
forall a b. a -> b
coe Bool
v4
then (Integer -> Integer -> [Integer] -> [Integer])
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> [Integer] -> [Integer]
du_aux_36 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60 (Integer
0 :: Integer)
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v3 Integer
v0)
((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
((Integer -> Integer -> Integer) -> Any -> Any -> Any
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
v1)
((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
2 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)))
([Integer] -> Any
forall a b. a -> b
coe [Integer]
v2))
else (Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
((Integer -> Integer -> Integer) -> Any -> Any -> Any
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
v1)
((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
2 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)))
([Integer] -> Any
forall a b. a -> b
coe [Integer]
v2)))
d_Expansion_62 :: Integer -> ()
d_Expansion_62 :: Integer -> ()
d_Expansion_62 = Integer -> ()
forall a. a
erased
d_fromDigits_68 ::
Integer -> [MAlonzo.Code.Data.Fin.Base.T_Fin_10] -> Integer
d_fromDigits_68 :: Integer -> [T_Fin_10] -> Integer
d_fromDigits_68 Integer
v0 [T_Fin_10]
v1
= case [T_Fin_10] -> [Any]
forall a b. a -> b
coe [T_Fin_10]
v1 of
[] -> Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
(:) Any
v2 [Any]
v3
-> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt ((T_Fin_10 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> Integer
MAlonzo.Code.Data.Fin.Base.du_toℕ_18 (Any -> Any
forall a b. a -> b
coe Any
v2))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt ((Integer -> [T_Fin_10] -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> [T_Fin_10] -> Integer
d_fromDigits_68 (Integer -> Any
forall a b. a -> b
coe Integer
v0) ([Any] -> Any
forall a b. a -> b
coe [Any]
v3)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
[Any]
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
d_toDigits_84 ::
Integer ->
AgdaAny -> Integer -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_toDigits_84 :: Integer -> Any -> Integer -> T_Σ_14
d_toDigits_84 Integer
v0 ~Any
v1 Integer
v2 = Integer -> Integer -> T_Σ_14
du_toDigits_84 Integer
v0 Integer
v2
du_toDigits_84 ::
Integer -> Integer -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_toDigits_84 :: Integer -> Integer -> T_Σ_14
du_toDigits_84 Integer
v0 Integer
v1
= 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
2 :: Integer)) in
Any -> T_Σ_14
forall a b. a -> b
coe
(((Any -> ()) -> (Any -> (Any -> Any -> Any) -> Any) -> Any -> Any)
-> Any -> Any -> Integer -> Any
forall a b. a -> b
coe
(Any -> ()) -> (Any -> (Any -> Any -> Any) -> Any) -> Any -> Any
MAlonzo.Code.Induction.WellFounded.du_wfRec_168 Any
forall a. a
erased
((Integer
-> Integer
-> (Integer -> T__'8804''8242'__338 -> T_Σ_14)
-> T_Σ_14)
-> Any -> Any
forall a b. a -> b
coe Integer
-> Integer -> (Integer -> T__'8804''8242'__338 -> T_Σ_14) -> T_Σ_14
du_helper_166 (Integer -> Any
forall a b. a -> b
coe Integer
v2)) Integer
v1)
d_Pred_96 ::
Integer ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
Integer -> Integer -> ()
d_Pred_96 :: Integer -> () -> Integer -> Integer -> ()
d_Pred_96 = Integer -> () -> Integer -> Integer -> ()
forall a. a
erased
d_cons_106 ::
Integer ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
Integer ->
Integer ->
MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_cons_106 :: Integer -> () -> Integer -> Integer -> T_Fin_10 -> T_Σ_14 -> T_Σ_14
d_cons_106 ~Integer
v0 ~()
v1 ~Integer
v2 ~Integer
v3 T_Fin_10
v4 T_Σ_14
v5 = T_Fin_10 -> T_Σ_14 -> T_Σ_14
du_cons_106 T_Fin_10
v4 T_Σ_14
v5
du_cons_106 ::
MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_cons_106 :: T_Fin_10 -> T_Σ_14 -> T_Σ_14
du_cons_106 T_Fin_10
v0 T_Σ_14
v1
= case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v1 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v2 Any
v3
-> (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe
Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v0) (Any -> Any
forall a b. a -> b
coe Any
v2))
Any
forall a. a
erased
T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_lem'8242'_120 ::
Integer ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
Integer ->
Integer ->
Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lem'8242'_120 :: Integer -> () -> Integer -> Integer -> Integer -> T__'8801'__12
d_lem'8242'_120 = Integer -> () -> Integer -> Integer -> Integer -> T__'8801'__12
forall a. a
erased
d_lem_144 ::
Integer ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
Integer ->
Integer ->
Integer ->
Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804''8242'__338
d_lem_144 :: Integer
-> ()
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804''8242'__338
d_lem_144 ~Integer
v0 ~()
v1 ~Integer
v2 Integer
v3 Integer
v4 Integer
v5 = Integer -> Integer -> Integer -> T__'8804''8242'__338
du_lem_144 Integer
v3 Integer
v4 Integer
v5
du_lem_144 ::
Integer ->
Integer ->
Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804''8242'__338
du_lem_144 :: Integer -> Integer -> Integer -> T__'8804''8242'__338
du_lem_144 Integer
v0 Integer
v1 Integer
v2
= (Integer -> T__'8804'__22 -> T__'8804''8242'__338)
-> Any -> Any -> T__'8804''8242'__338
forall a b. a -> b
coe
Integer -> T__'8804'__22 -> T__'8804''8242'__338
MAlonzo.Code.Data.Nat.Properties.du_'8804''8658''8804''8242'_6128
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt ((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))
((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
2 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
(Integer -> Any
forall a b. a -> b
coe Integer
v2))
(((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_start_96
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v3 Any
v4 Any
v5 ->
(T__'8804'__22 -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_2854 Any
v5))
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt ((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))
((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
2 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
(Integer -> Integer
forall a b. a -> b
coe Integer
v2))
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Integer -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> Any -> (Any -> Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v3 Any
v4 Any
v5 Any
v6 Any
v7 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986 Any
v6
Any
v7))
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((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
2 :: Integer))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt ((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)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Integer
forall a b. a -> b
coe Integer
v2))
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt ((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))
((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
2 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
(Integer -> Integer
forall a b. a -> b
coe Integer
v2))
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Integer
-> Integer
-> Integer
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
(\ Any
v3 Any
v4 Any
v5 Any
v6 Any
v7 -> Any
v7)
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((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
2 :: Integer))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt ((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)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Integer
forall a b. a -> b
coe Integer
v2))
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((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
2 :: Integer))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt ((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)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Integer
forall a b. a -> b
coe Integer
v2))
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt ((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))
((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
2 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
(Integer -> Integer
forall a b. a -> b
coe Integer
v2))
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Integer
-> Integer
-> Integer
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10216'_448
(\ Any
v3 Any
v4 Any
v5 Any
v6 Any
v7 -> Any
v7)
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((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
2 :: Integer))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt ((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)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Integer
forall a b. a -> b
coe Integer
v2))
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((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
2 :: Integer))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt ((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)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Integer
forall a b. a -> b
coe Integer
v2))
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt ((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))
((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
2 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
(Integer -> Integer
forall a b. a -> b
coe Integer
v2))
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Integer
-> Integer
-> Integer
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
(\ Any
v3 Any
v4 Any
v5 Any
v6 Any
v7 -> Any
v7)
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((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
2 :: Integer))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt ((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)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Integer
forall a b. a -> b
coe Integer
v2))
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((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
2 :: Integer))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt ((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)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Integer
forall a b. a -> b
coe Integer
v2))
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt ((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))
((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
2 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
(Integer -> Integer
forall a b. a -> b
coe Integer
v2))
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Integer
-> Integer
-> Integer
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
(\ Any
v3 Any
v4 Any
v5 Any
v6 Any
v7 -> Any
v7)
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((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
2 :: Integer))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt ((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)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Integer
forall a b. a -> b
coe Integer
v2))
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((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
2 :: Integer))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt ((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)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Integer
forall a b. a -> b
coe Integer
v2))
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt ((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))
((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
2 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
(Integer -> Integer
forall a b. a -> b
coe Integer
v2))
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Integer
-> Integer
-> Integer
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10216'_448
(\ Any
v3 Any
v4 Any
v5 Any
v6 Any
v7 -> Any
v7)
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((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
2 :: Integer))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt ((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))
(Integer -> Any
forall a b. a -> b
coe Integer
v1)))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Integer
forall a b. a -> b
coe Integer
v2))
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((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
2 :: Integer))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt ((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))
(Integer -> Any
forall a b. a -> b
coe Integer
v1)))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Integer
forall a b. a -> b
coe Integer
v2))
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt ((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))
((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
2 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
(Integer -> Integer
forall a b. a -> b
coe Integer
v2))
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Integer
-> Integer
-> Integer
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
(\ Any
v3 Any
v4 Any
v5 Any
v6 Any
v7 -> Any
v7)
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((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
2 :: Integer))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt ((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))
(Integer -> Any
forall a b. a -> b
coe Integer
v1)))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Integer
forall a b. a -> b
coe Integer
v2))
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((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
2 :: Integer))
((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
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
2 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v1))))
(Integer -> Any
forall a b. a -> b
coe Integer
v1))
(Integer -> Integer
forall a b. a -> b
coe Integer
v2))
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt ((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))
((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
2 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
(Integer -> Integer
forall a b. a -> b
coe Integer
v2))
(((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt ((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))
((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
2 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
(Integer -> Any
forall a b. a -> b
coe Integer
v2)))
Any
forall a. a
erased)
Any
forall a. a
erased)
Any
forall a. a
erased)
Any
forall a. a
erased)
Any
forall a. a
erased)
Any
forall a. a
erased)
((Integer -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_m'8804'm'43'n_3482
((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
2 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)))))
d_helper_166 ::
Integer ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
Integer ->
Integer ->
(Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804''8242'__338 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_helper_166 :: Integer
-> ()
-> Integer
-> Integer
-> (Integer -> T__'8804''8242'__338 -> T_Σ_14)
-> T_Σ_14
d_helper_166 Integer
v0 ~()
v1 ~Integer
v2 Integer
v3 Integer -> T__'8804''8242'__338 -> T_Σ_14
v4 = Integer
-> Integer -> (Integer -> T__'8804''8242'__338 -> T_Σ_14) -> T_Σ_14
du_helper_166 Integer
v0 Integer
v3 Integer -> T__'8804''8242'__338 -> T_Σ_14
v4
du_helper_166 ::
Integer ->
Integer ->
(Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804''8242'__338 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_helper_166 :: Integer
-> Integer -> (Integer -> T__'8804''8242'__338 -> T_Σ_14) -> T_Σ_14
du_helper_166 Integer
v0 Integer
v1 Integer -> T__'8804''8242'__338 -> T_Σ_14
v2
= let v3 :: t
v3
= (Integer -> Integer -> Integer) -> Any -> Any -> t
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
v1)
((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
2 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)) in
Any -> T_Σ_14
forall a b. a -> b
coe
(let v4 :: t
v4
= (Integer -> Integer -> T_Fin_10) -> Any -> Any -> t
forall a b. a -> b
coe
Integer -> Integer -> T_Fin_10
MAlonzo.Code.Data.Nat.DivMod.du__mod__1162 (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
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
2 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)) in
Any -> Any
forall a b. a -> b
coe
(case Any -> Integer
forall a b. a -> b
coe Any
forall a. a
v3 of
Integer
0 -> (Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((Any -> [Any]) -> Any -> Any
forall a b. a -> b
coe Any -> [Any]
MAlonzo.Code.Data.List.Base.du_'91'_'93'_286 (Any -> Any
forall a b. a -> b
coe Any
forall a. a
v4)) Any
forall a. a
erased
Integer
_ -> let v5 :: Integer
v5 = Integer -> Integer -> Integer
subInt (Any -> Integer
forall a b. a -> b
coe Any
forall a. a
v3) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Any
forall a b. a -> b
coe
((T_Fin_10 -> T_Σ_14 -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Fin_10 -> T_Σ_14 -> T_Σ_14
du_cons_106 (Any -> Any
forall a b. a -> b
coe Any
forall a. a
v4)
((Integer -> T__'8804''8242'__338 -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804''8242'__338 -> T_Σ_14
v2 Any
forall a. a
v3
((Integer -> Integer -> Integer -> T__'8804''8242'__338)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> T__'8804''8242'__338
du_lem_144 (Integer -> Any
forall a b. a -> b
coe Integer
v5) (Integer -> Any
forall a b. a -> b
coe Integer
v0)
((T_Fin_10 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> Integer
MAlonzo.Code.Data.Fin.Base.du_toℕ_18 (Any -> Any
forall a b. a -> b
coe Any
forall a. a
v4)))))))
d_digitChars_192 :: MAlonzo.Code.Data.Vec.Base.T_Vec_28
d_digitChars_192 :: T_Vec_28
d_digitChars_192
= (Any -> T_Vec_28 -> T_Vec_28) -> Char -> Any -> T_Vec_28
forall a b. a -> b
coe
Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Char
'0'
((Any -> T_Vec_28 -> T_Vec_28) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Char
'1'
((Any -> T_Vec_28 -> T_Vec_28) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Char
'2'
((Any -> T_Vec_28 -> T_Vec_28) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Char
'3'
((Any -> T_Vec_28 -> T_Vec_28) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Char
'4'
((Any -> T_Vec_28 -> T_Vec_28) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Char
'5'
((Any -> T_Vec_28 -> T_Vec_28) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Char
'6'
((Any -> T_Vec_28 -> T_Vec_28) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Char
'7'
((Any -> T_Vec_28 -> T_Vec_28) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Char
'8'
((Any -> T_Vec_28 -> T_Vec_28) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Char
'9'
((Any -> T_Vec_28 -> T_Vec_28) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Char
'a'
((Any -> T_Vec_28 -> T_Vec_28) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Char
'b'
((Any -> T_Vec_28 -> T_Vec_28) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Char
'c'
((Any -> T_Vec_28 -> T_Vec_28) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Char
'd'
((Any -> T_Vec_28 -> T_Vec_28) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Char
'e'
((Any -> T_Vec_28 -> T_Vec_28) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Char
'f'
(T_Vec_28 -> Any
forall a b. a -> b
coe
T_Vec_28
MAlonzo.Code.Data.Vec.Base.C_'91''93'_32))))))))))))))))
d_showDigit_198 ::
Integer ->
AgdaAny ->
MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6
d_showDigit_198 :: Integer -> Any -> T_Fin_10 -> Char
d_showDigit_198 ~Integer
v0 ~Any
v1 T_Fin_10
v2 = T_Fin_10 -> Char
du_showDigit_198 T_Fin_10
v2
du_showDigit_198 ::
MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6
du_showDigit_198 :: T_Fin_10 -> Char
du_showDigit_198 T_Fin_10
v0
= (T_Vec_28 -> T_Fin_10 -> Any) -> Any -> Any -> Char
forall a b. a -> b
coe
T_Vec_28 -> T_Fin_10 -> Any
MAlonzo.Code.Data.Vec.Base.du_lookup_82 (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
d_digitChars_192)
(T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v0)