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

-- 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_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
-- Data.Digit.1b
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)
-- 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_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))
-- Data.Digit._.aux
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)))
-- Data.Digit._._.q<n
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))
-- Data.Digit.Expansion
d_Expansion_76 :: Integer -> ()
d_Expansion_76 :: Integer -> ()
d_Expansion_76 = Integer -> ()
forall a. a
erased
-- Data.Digit.fromDigits
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
-- Data.Digit.toDigits
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)
-- Data.Digit._.base
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)
-- Data.Digit._.Pred
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
-- Data.Digit._.cons
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
-- Data.Digit._.lem
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)))))
-- Data.Digit._.helper
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))))))
-- Data.Digit.digitChars
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))))))))))))))))
-- Data.Digit.showDigit
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)