{-# 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.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
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_6
d_0b_12 :: T_Fin_6
d_0b_12 = T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10
d_1b_14 :: MAlonzo.Code.Data.Fin.Base.T_Fin_6
d_1b_14 :: T_Fin_6
d_1b_14
= (T_Fin_6 -> T_Fin_6) -> Any -> T_Fin_6
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
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_306 (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_38 (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_38 ::
Integer ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
Integer ->
Integer ->
MAlonzo.Code.Induction.WellFounded.T_Acc_42 ->
[Integer] -> [Integer]
d_aux_38 :: Integer
-> () -> Integer -> Integer -> T_Acc_42 -> [Integer] -> [Integer]
d_aux_38 Integer
v0 ~()
v1 ~Integer
v2 Integer
v3 ~T_Acc_42
v4 [Integer]
v5 = Integer -> Integer -> [Integer] -> [Integer]
du_aux_38 Integer
v0 Integer
v3 [Integer]
v5
du_aux_38 :: Integer -> Integer -> [Integer] -> [Integer]
du_aux_38 :: Integer -> Integer -> [Integer] -> [Integer]
du_aux_38 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_38 (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
MAlonzo.Code.Data.Nat.DivMod.du__'47'__56 (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)))
((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.DivMod.du__'37'__68 (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.DivMod.du__'37'__68 (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_q'60'n_74 ::
Integer ->
Integer ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
Integer ->
(Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
MAlonzo.Code.Induction.WellFounded.T_Acc_42) ->
[Integer] -> MAlonzo.Code.Data.Nat.Base.T__'8804'__18
d_q'60'n_74 :: Integer
-> Integer
-> ()
-> Integer
-> (Integer -> T__'8804'__18 -> T_Acc_42)
-> [Integer]
-> T__'8804'__18
d_q'60'n_74 Integer
v0 Integer
v1 ~()
v2 ~Integer
v3 ~Integer -> T__'8804'__18 -> T_Acc_42
v4 ~[Integer]
v5 = Integer -> Integer -> T__'8804'__18
du_q'60'n_74 Integer
v0 Integer
v1
du_q'60'n_74 ::
Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__18
du_q'60'n_74 :: Integer -> Integer -> T__'8804'__18
du_q'60'n_74 Integer
v0 Integer
v1
= (Integer -> Integer -> T__'8804'__18)
-> Any -> Any -> T__'8804'__18
forall a b. a -> b
coe
Integer -> Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.DivMod.du_m'47'n'60'm_492
((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
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))
d_Expansion_76 :: Integer -> ()
d_Expansion_76 :: Integer -> ()
d_Expansion_76 = Integer -> ()
forall a. a
erased
d_fromDigits_82 ::
Integer -> [MAlonzo.Code.Data.Fin.Base.T_Fin_6] -> Integer
d_fromDigits_82 :: Integer -> [T_Fin_6] -> Integer
d_fromDigits_82 Integer
v0 [T_Fin_6]
v1
= case [T_Fin_6] -> [Any]
forall a b. a -> b
coe [T_Fin_6]
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_6 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Fin_6 -> Integer
MAlonzo.Code.Data.Fin.Base.du_toℕ_20 (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_6] -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> [T_Fin_6] -> Integer
d_fromDigits_82 (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_98 ::
Integer ->
AgdaAny -> Integer -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_toDigits_98 :: Integer -> Any -> Integer -> T_Σ_14
d_toDigits_98 Integer
v0 ~Any
v1 Integer
v2 = Integer -> Integer -> T_Σ_14
du_toDigits_98 Integer
v0 Integer
v2
du_toDigits_98 ::
Integer -> Integer -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_toDigits_98 :: Integer -> Integer -> T_Σ_14
du_toDigits_98 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_164 Any
forall a. a
erased
((Integer
-> Integer
-> (Integer -> T__'8804''8242'__154 -> T_Σ_14)
-> T_Σ_14)
-> Any -> Any
forall a b. a -> b
coe Integer
-> Integer -> (Integer -> T__'8804''8242'__154 -> T_Σ_14) -> T_Σ_14
du_helper_152 (Integer -> Any
forall a b. a -> b
coe Integer
v2)) Integer
v1)
d_base_108 ::
Integer ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 -> Integer -> Integer
d_base_108 :: Integer -> () -> Integer -> Integer
d_base_108 Integer
v0 ~()
v1 ~Integer
v2 = Integer -> Integer
du_base_108 Integer
v0
du_base_108 :: Integer -> Integer
du_base_108 :: Integer -> Integer
du_base_108 Integer
v0 = (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
2 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)
d_Pred_110 ::
Integer ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
Integer -> Integer -> ()
d_Pred_110 :: Integer -> () -> Integer -> Integer -> ()
d_Pred_110 = Integer -> () -> Integer -> Integer -> ()
forall a. a
erased
d_cons_120 ::
Integer ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
Integer ->
Integer ->
MAlonzo.Code.Data.Fin.Base.T_Fin_6 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_cons_120 :: Integer -> () -> Integer -> Integer -> T_Fin_6 -> T_Σ_14 -> T_Σ_14
d_cons_120 ~Integer
v0 ~()
v1 ~Integer
v2 ~Integer
v3 T_Fin_6
v4 T_Σ_14
v5 = T_Fin_6 -> T_Σ_14 -> T_Σ_14
du_cons_120 T_Fin_6
v4 T_Σ_14
v5
du_cons_120 ::
MAlonzo.Code.Data.Fin.Base.T_Fin_6 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_cons_120 :: T_Fin_6 -> T_Σ_14 -> T_Σ_14
du_cons_120 T_Fin_6
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_6 -> Any
forall a b. a -> b
coe T_Fin_6
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_136 ::
Integer ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
Integer ->
Integer ->
Integer ->
Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804''8242'__154
d_lem_136 :: Integer
-> ()
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804''8242'__154
d_lem_136 ~Integer
v0 ~()
v1 ~Integer
v2 Integer
v3 Integer
v4 Integer
v5 = Integer -> Integer -> Integer -> T__'8804''8242'__154
du_lem_136 Integer
v3 Integer
v4 Integer
v5
du_lem_136 ::
Integer ->
Integer ->
Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804''8242'__154
du_lem_136 :: Integer -> Integer -> Integer -> T__'8804''8242'__154
du_lem_136 Integer
v0 Integer
v1 Integer
v2
= (Integer -> T__'8804'__18 -> T__'8804''8242'__154)
-> Any -> Any -> T__'8804''8242'__154
forall a b. a -> b
coe
Integer -> T__'8804'__18 -> T__'8804''8242'__154
MAlonzo.Code.Data.Nat.Properties.du_'8804''8658''8804''8242'_4640
((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))
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_begin__160
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v3 Any
v4 Any
v5 ->
(Integer -> T__'8804'__18 -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_1736 Any
v4 Any
v5)
((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 -> 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))
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> 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
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v3 Any
v4 Any
v5 Any
v6 Any
v7 ->
(T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868 Any
v6 Any
v7)
((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 -> 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 -> 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 -> Any
forall a b. a -> b
coe Integer
v2))
((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))
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__70) -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du__'8718'_346
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
((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)))
((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_m'8804'm'43'n_2316
((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_152 ::
Integer ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
Integer ->
Integer ->
(Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804''8242'__154 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_helper_152 :: Integer
-> ()
-> Integer
-> Integer
-> (Integer -> T__'8804''8242'__154 -> T_Σ_14)
-> T_Σ_14
d_helper_152 Integer
v0 ~()
v1 ~Integer
v2 Integer
v3 Integer -> T__'8804''8242'__154 -> T_Σ_14
v4 = Integer
-> Integer -> (Integer -> T__'8804''8242'__154 -> T_Σ_14) -> T_Σ_14
du_helper_152 Integer
v0 Integer
v3 Integer -> T__'8804''8242'__154 -> T_Σ_14
v4
du_helper_152 ::
Integer ->
Integer ->
(Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804''8242'__154 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_helper_152 :: Integer
-> Integer -> (Integer -> T__'8804''8242'__154 -> T_Σ_14) -> T_Σ_14
du_helper_152 Integer
v0 Integer
v1 Integer -> T__'8804''8242'__154 -> 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.DivMod.du__'47'__56 (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_6) -> Any -> Any -> t
forall a b. a -> b
coe
Integer -> Integer -> T_Fin_6
MAlonzo.Code.Data.Nat.DivMod.du__mod__842 (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'_298 (Any -> Any
forall a b. a -> b
coe Any
forall a. a
v4)) Any
forall a. a
erased
Integer
_ -> (T_Fin_6 -> T_Σ_14 -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Fin_6 -> T_Σ_14 -> T_Σ_14
du_cons_120 (Any -> Any
forall a b. a -> b
coe Any
forall a. a
v4)
((Integer -> T__'8804''8242'__154 -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804''8242'__154 -> T_Σ_14
v2 Any
forall a. a
v3
((Integer -> Integer -> Integer -> T__'8804''8242'__154)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> T__'8804''8242'__154
du_lem_136 ((Integer -> Integer) -> Any -> Any
forall a b. a -> b
coe Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d_pred_94 (Any -> Any
forall a b. a -> b
coe Any
forall a. a
v3))
(Integer -> Any
forall a b. a -> b
coe Integer
v0) ((T_Fin_6 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Fin_6 -> Integer
MAlonzo.Code.Data.Fin.Base.du_toℕ_20 (Any -> Any
forall a b. a -> b
coe Any
forall a. a
v4))))))
d_digitChars_172 :: MAlonzo.Code.Data.Vec.Base.T_Vec_24
d_digitChars_172 :: T_Vec_24
d_digitChars_172
= (Any -> T_Vec_24 -> T_Vec_24) -> Char -> Any -> T_Vec_24
forall a b. a -> b
coe
Any -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.C__'8759'__36 Char
'0'
((Any -> T_Vec_24 -> T_Vec_24) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.C__'8759'__36 Char
'1'
((Any -> T_Vec_24 -> T_Vec_24) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.C__'8759'__36 Char
'2'
((Any -> T_Vec_24 -> T_Vec_24) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.C__'8759'__36 Char
'3'
((Any -> T_Vec_24 -> T_Vec_24) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.C__'8759'__36 Char
'4'
((Any -> T_Vec_24 -> T_Vec_24) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.C__'8759'__36 Char
'5'
((Any -> T_Vec_24 -> T_Vec_24) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.C__'8759'__36 Char
'6'
((Any -> T_Vec_24 -> T_Vec_24) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.C__'8759'__36 Char
'7'
((Any -> T_Vec_24 -> T_Vec_24) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.C__'8759'__36 Char
'8'
((Any -> T_Vec_24 -> T_Vec_24) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.C__'8759'__36 Char
'9'
((Any -> T_Vec_24 -> T_Vec_24) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.C__'8759'__36 Char
'a'
((Any -> T_Vec_24 -> T_Vec_24) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.C__'8759'__36 Char
'b'
((Any -> T_Vec_24 -> T_Vec_24) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.C__'8759'__36 Char
'c'
((Any -> T_Vec_24 -> T_Vec_24) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.C__'8759'__36 Char
'd'
((Any -> T_Vec_24 -> T_Vec_24) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.C__'8759'__36 Char
'e'
((Any -> T_Vec_24 -> T_Vec_24) -> Char -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.C__'8759'__36 Char
'f'
(T_Vec_24 -> Any
forall a b. a -> b
coe
T_Vec_24
MAlonzo.Code.Data.Vec.Base.C_'91''93'_28))))))))))))))))
d_showDigit_178 ::
Integer ->
AgdaAny ->
MAlonzo.Code.Data.Fin.Base.T_Fin_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6
d_showDigit_178 :: Integer -> Any -> T_Fin_6 -> Char
d_showDigit_178 ~Integer
v0 ~Any
v1 T_Fin_6
v2 = T_Fin_6 -> Char
du_showDigit_178 T_Fin_6
v2
du_showDigit_178 ::
MAlonzo.Code.Data.Fin.Base.T_Fin_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6
du_showDigit_178 :: T_Fin_6 -> Char
du_showDigit_178 T_Fin_6
v0
= (T_Vec_24 -> T_Fin_6 -> Any) -> Any -> Any -> Char
forall a b. a -> b
coe
T_Vec_24 -> T_Fin_6 -> Any
MAlonzo.Code.Data.Vec.Base.du_lookup_94 (T_Vec_24 -> Any
forall a b. a -> b
coe T_Vec_24
d_digitChars_172)
(T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v0)