{-# 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

-- Data.Digit.Digit
d_Digit_4 :: Integer -> ()
d_Digit_4 :: Integer -> ()
d_Digit_4 = Integer -> ()
forall a. a
erased
-- Data.Digit.Decimal
d_Decimal_8 :: ()
d_Decimal_8 :: ()
d_Decimal_8 = ()
forall a. a
erased
-- Data.Digit.Bit
d_Bit_10 :: ()
d_Bit_10 :: ()
d_Bit_10 = ()
forall a. a
erased
-- Data.Digit.0b
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
-- Data.Digit.1b
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)
-- Data.Digit.toNatDigits
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))
-- Data.Digit._.aux
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)))
-- Data.Digit.Expansion
d_Expansion_62 :: Integer -> ()
d_Expansion_62 :: Integer -> ()
d_Expansion_62 = Integer -> ()
forall a. a
erased
-- Data.Digit.fromDigits
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
-- Data.Digit.toDigits
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)
-- Data.Digit._.Pred
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
-- Data.Digit._.cons
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
-- Data.Digit._.lem′
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
-- Data.Digit._.lem
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)))))
-- Data.Digit._.helper
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)))))))
-- Data.Digit.digitChars
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))))))))))))))))
-- Data.Digit.showDigit
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)