{-# 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.VerifiedCompilation.UCaseReduce 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.Equality
import qualified MAlonzo.Code.Agda.Builtin.List
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Builtin.Signature
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.RawU
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects
import qualified MAlonzo.Code.Untyped
import qualified MAlonzo.Code.Untyped.CEK
import qualified MAlonzo.Code.VerifiedCompilation.Certificate
import qualified MAlonzo.Code.VerifiedCompilation.Equality
import qualified MAlonzo.Code.VerifiedCompilation.UntypedTranslation
import qualified MAlonzo.Code.VerifiedCompilation.UntypedViews

-- VerifiedCompilation.UCaseReduce.iterApp
d_iterApp_6 ::
  () ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  MAlonzo.Code.Untyped.T__'8866'_14
d_iterApp_6 :: () -> T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
d_iterApp_6 ~()
v0 T__'8866'_14
v1 [T__'8866'_14]
v2 = T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
du_iterApp_6 T__'8866'_14
v1 [T__'8866'_14]
v2
du_iterApp_6 ::
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  MAlonzo.Code.Untyped.T__'8866'_14
du_iterApp_6 :: T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
du_iterApp_6 T__'8866'_14
v0 [T__'8866'_14]
v1
  = case [T__'8866'_14] -> [Any]
forall a b. a -> b
coe [T__'8866'_14]
v1 of
      [] -> T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v0
      (:) Any
v2 [Any]
v3
        -> (T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> Any -> Any -> T__'8866'_14
forall a b. a -> b
coe
             T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
du_iterApp_6
             ((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v0) (Any -> Any
forall a b. a -> b
coe Any
v2)) ([Any] -> Any
forall a b. a -> b
coe [Any]
v3)
      [Any]
_ -> T__'8866'_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.UCaseReduce.CaseReduce
d_CaseReduce_16 :: p -> p -> p -> p -> ()
d_CaseReduce_16 p
a0 p
a1 p
a2 p
a3 = ()
data T_CaseReduce_16
  = C_casereduce_32 MAlonzo.Code.Untyped.T__'8866'_14
                    MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_16
-- VerifiedCompilation.UCaseReduce.isCaseReduce?
d_isCaseReduce'63'_42 ::
  () ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_26
d_isCaseReduce'63'_42 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
d_isCaseReduce'63'_42 ~()
v0 T_DecEq_6
v1 = T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isCaseReduce'63'_42 T_DecEq_6
v1
du_isCaseReduce'63'_42 ::
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_26
du_isCaseReduce'63'_42 :: T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isCaseReduce'63'_42 T_DecEq_6
v0
  = (()
 -> T_DecEq_6
 -> T_SimplifierTag_4
 -> (()
     -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26)
 -> T__'8866'_14
 -> T__'8866'_14
 -> T_ProofOrCE_26)
-> Any
-> Any
-> Any
-> (Any -> Any -> Any -> Any -> Any)
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_26
forall a b. a -> b
coe
      ()
-> T_DecEq_6
-> T_SimplifierTag_4
-> (()
    -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26)
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_translation'63'_178
      Any
forall a. a
erased (T_DecEq_6 -> Any
forall a b. a -> b
coe T_DecEq_6
v0)
      (T_SimplifierTag_4 -> Any
forall a b. a -> b
coe T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_caseReduceT_12)
      (\ Any
v1 Any
v2 Any
v3 Any
v4 -> (T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isCR'63'_60 Any
v2 Any
v3 Any
v4)
-- VerifiedCompilation.UCaseReduce.justEq
d_justEq_50 ::
  () ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_justEq_50 :: () -> Any -> Any -> T__'8801'__12 -> T__'8801'__12
d_justEq_50 = () -> Any -> Any -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
-- VerifiedCompilation.UCaseReduce.isCR?
d_isCR'63'_60 ::
  () ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_26
d_isCR'63'_60 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
d_isCR'63'_60 ~()
v0 T_DecEq_6
v1 T__'8866'_14
v2 T__'8866'_14
v3 = T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isCR'63'_60 T_DecEq_6
v1 T__'8866'_14
v2 T__'8866'_14
v3
du_isCR'63'_60 ::
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_26
du_isCR'63'_60 :: T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isCR'63'_60 T_DecEq_6
v0 T__'8866'_14
v1 T__'8866'_14
v2
  = let v3 :: t
v3
          = (()
 -> (() -> T__'8866'_14 -> T_Dec_20)
 -> (() -> [T__'8866'_14] -> T_Dec_20)
 -> T__'8866'_14
 -> T_Dec_20)
-> Any -> Any -> (Any -> Any -> Any) -> Any -> t
forall a b. a -> b
coe
              ()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> [T__'8866'_14] -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isCase'63'_598
              Any
forall a. a
erased
              ((Any -> Any) -> Any
forall a b. a -> b
coe
                 (\ Any
v3 ->
                    (()
 -> (() -> [T__'8866'_14] -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> Any -> (Any -> Any -> Any) -> Any
forall a b. a -> b
coe
                      ()
-> (() -> [T__'8866'_14] -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isConstr'63'_496
                      Any
forall a. a
erased
                      (\ Any
v4 Any
v5 ->
                         T_Dec_20 -> Any
forall a b. a -> b
coe
                           T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_allTerms'63'_798)))
              (\ Any
v3 Any
v4 ->
                 T_Dec_20 -> Any
forall a b. a -> b
coe
                   T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_allTerms'63'_798)
              (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1) in
    Any -> T_ProofOrCE_26
forall a b. a -> b
coe
      (case Any -> T_Dec_20
forall a b. a -> b
coe Any
forall a. a
v3 of
         MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v4 T_Reflects_16
v5
           -> if Bool -> Bool
forall a b. a -> b
coe Bool
v4
                then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v5 of
                       MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v6
                         -> case Any -> T_isCase_574
forall a b. a -> b
coe Any
v6 of
                              MAlonzo.Code.VerifiedCompilation.UntypedViews.C_iscase_586 Any
v9 Any
v10
                                -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
                                     MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v11 [T__'8866'_14]
v12
                                       -> case Any -> T_isConstr_478
forall a b. a -> b
coe Any
v9 of
                                            MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isconstr_488 Any
v15
                                              -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v11 of
                                                   MAlonzo.Code.Untyped.C_constr_34 Integer
v16 [T__'8866'_14]
v17
                                                     -> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                          Any -> Any -> Any
forall a b. a -> b -> b
seq (Any -> Any
forall a b. a -> b
coe Any
v15)
                                                          ((Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                             Any -> Any -> Any
forall a b. a -> b -> b
seq (Any -> Any
forall a b. a -> b
coe Any
v10)
                                                             (let v18 :: t
v18
                                                                    = (Integer -> [Any] -> Maybe Any) -> Any -> Any -> t
forall a b. a -> b
coe
                                                                        Integer -> [Any] -> Maybe Any
MAlonzo.Code.Untyped.CEK.du_lookup'63'_946
                                                                        (Integer -> Any
forall a b. a -> b
coe Integer
v16) ([T__'8866'_14] -> Any
forall a b. a -> b
coe [T__'8866'_14]
v12) in
                                                              Any -> Any
forall a b. a -> b
coe
                                                                (case Any -> Maybe Any
forall a b. a -> b
coe Any
forall a. a
v18 of
                                                                   MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v19
                                                                     -> let v20 :: t
v20
                                                                              = (T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26)
-> T_DecEq_6 -> Any -> T__'8866'_14 -> t
forall a b. a -> b
coe
                                                                                  T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isCaseReduce'63'_42
                                                                                  T_DecEq_6
v0
                                                                                  ((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                     T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
du_iterApp_6
                                                                                     (Any -> Any
forall a b. a -> b
coe Any
v19)
                                                                                     ([T__'8866'_14] -> Any
forall a b. a -> b
coe [T__'8866'_14]
v17))
                                                                                  T__'8866'_14
v2 in
                                                                        Any -> Any
forall a b. a -> b
coe
                                                                          (case Any -> T_ProofOrCE_26
forall a b. a -> b
coe Any
forall a. a
v20 of
                                                                             MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_32 Any
v21
                                                                               -> (Any -> T_ProofOrCE_26) -> Any -> Any
forall a b. a -> b
coe
                                                                                    Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_32
                                                                                    ((T__'8866'_14 -> T_Translation_16 -> T_CaseReduce_16)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                       T__'8866'_14 -> T_Translation_16 -> T_CaseReduce_16
C_casereduce_32
                                                                                       Any
v19 Any
v21)
                                                                             MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40 T_SimplifierTag_4
v24 Any
v25 Any
v26
                                                                               -> (T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26)
-> T_SimplifierTag_4 -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                    T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40
                                                                                    T_SimplifierTag_4
v24 Any
v25 Any
v26
                                                                             T_ProofOrCE_26
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
                                                                   Maybe Any
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
                                                                     -> (T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26)
-> Any -> T__'8866'_14 -> T__'8866'_14 -> Any
forall a b. a -> b
coe
                                                                          T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40
                                                                          (T_SimplifierTag_4 -> Any
forall a b. a -> b
coe
                                                                             T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_caseReduceT_12)
                                                                          T__'8866'_14
v1 T__'8866'_14
v2
                                                                   Maybe Any
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)))
                                                   T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                            T_isConstr_478
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                     T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                              T_isCase_574
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                       T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                       Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v5)
                       ((T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26)
-> Any -> T__'8866'_14 -> T__'8866'_14 -> Any
forall a b. a -> b
coe
                          T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40
                          (T_SimplifierTag_4 -> Any
forall a b. a -> b
coe T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_caseReduceT_12)
                          T__'8866'_14
v1 T__'8866'_14
v2)
         T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- VerifiedCompilation.UCaseReduce..extendedlambda0
d_'46'extendedlambda0_76 ::
  () ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  (MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isCase_574 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  T_CaseReduce_16 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda0_76 :: ()
-> T__'8866'_14
-> (T_isCase_574 -> T_Irrelevant_20)
-> T_DecEq_6
-> T__'8866'_14
-> T_CaseReduce_16
-> T_Irrelevant_20
d_'46'extendedlambda0_76 = ()
-> T__'8866'_14
-> (T_isCase_574 -> T_Irrelevant_20)
-> T_DecEq_6
-> T__'8866'_14
-> T_CaseReduce_16
-> T_Irrelevant_20
forall a. a
erased
-- VerifiedCompilation.UCaseReduce..extendedlambda1
d_'46'extendedlambda1_104 ::
  () ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  Integer ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  T_CaseReduce_16 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda1_104 :: ()
-> [T__'8866'_14]
-> Integer
-> T__'8801'__12
-> [T__'8866'_14]
-> T_DecEq_6
-> T__'8866'_14
-> T_CaseReduce_16
-> T_Irrelevant_20
d_'46'extendedlambda1_104 = ()
-> [T__'8866'_14]
-> Integer
-> T__'8801'__12
-> [T__'8866'_14]
-> T_DecEq_6
-> T__'8866'_14
-> T_CaseReduce_16
-> T_Irrelevant_20
forall a. a
erased
-- VerifiedCompilation.UCaseReduce..extendedlambda2
d_'46'extendedlambda2_108 ::
  () ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  Integer ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_16 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda2_108 :: ()
-> [T__'8866'_14]
-> Integer
-> T__'8801'__12
-> [T__'8866'_14]
-> T_DecEq_6
-> T__'8866'_14
-> T__'8866'_14
-> T__'8801'__12
-> T_Translation_16
-> T__'8801'__12
-> T_Irrelevant_20
d_'46'extendedlambda2_108 = ()
-> [T__'8866'_14]
-> Integer
-> T__'8801'__12
-> [T__'8866'_14]
-> T_DecEq_6
-> T__'8866'_14
-> T__'8866'_14
-> T__'8801'__12
-> T_Translation_16
-> T__'8801'__12
-> T_Irrelevant_20
forall a. a
erased
-- VerifiedCompilation.UCaseReduce..extendedlambda3
d_'46'extendedlambda3_160 ::
  () ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  (MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_16 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  () ->
  () ->
  MAlonzo.Code.VerifiedCompilation.Certificate.T_SimplifierTag_4 ->
  AgdaAny ->
  AgdaAny ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  Integer ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T_CaseReduce_16 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda3_160 :: ()
-> T__'8866'_14
-> [T__'8866'_14]
-> T_DecEq_6
-> T__'8866'_14
-> (T_Translation_16 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> [T__'8866'_14]
-> Integer
-> T__'8801'__12
-> T_CaseReduce_16
-> T_Irrelevant_20
d_'46'extendedlambda3_160 = ()
-> T__'8866'_14
-> [T__'8866'_14]
-> T_DecEq_6
-> T__'8866'_14
-> (T_Translation_16 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> [T__'8866'_14]
-> Integer
-> T__'8801'__12
-> T_CaseReduce_16
-> T_Irrelevant_20
forall a. a
erased
-- VerifiedCompilation.UCaseReduce.UCaseReduce
d_UCaseReduce_168 ::
  () ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 -> ()
d_UCaseReduce_168 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> ()
d_UCaseReduce_168 = () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> ()
forall a. a
erased
-- VerifiedCompilation.UCaseReduce.integer
d_integer_170 :: MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4
d_integer_170 :: T__'8866''9839'_4
d_integer_170
  = (T_Tag_28 Any -> T__'8866''9839'_4) -> Any -> T__'8866''9839'_4
forall a b. a -> b
coe
      T_Tag_28 Any -> T__'8866''9839'_4
MAlonzo.Code.RawU.du_tag2TyTag_206
      (DefaultUni (Esc Integer) -> Any
forall a b. a -> b
coe DefaultUni (Esc Integer)
forall {a}. (a ~ Esc Integer) => DefaultUni a
MAlonzo.Code.RawU.C_integer_30)
-- VerifiedCompilation.UCaseReduce.con-integer
d_con'45'integer_174 ::
  () -> Integer -> MAlonzo.Code.Untyped.T__'8866'_14
d_con'45'integer_174 :: () -> Integer -> T__'8866'_14
d_con'45'integer_174 ~()
v0 Integer
v1 = Integer -> T__'8866'_14
du_con'45'integer_174 Integer
v1
du_con'45'integer_174 ::
  Integer -> MAlonzo.Code.Untyped.T__'8866'_14
du_con'45'integer_174 :: Integer -> T__'8866'_14
du_con'45'integer_174 Integer
v0
  = (T_TmCon_198 -> T__'8866'_14) -> Any -> T__'8866'_14
forall a b. a -> b
coe
      T_TmCon_198 -> T__'8866'_14
MAlonzo.Code.Untyped.C_con_28
      ((T__'8866''9839'_4 -> Any -> T_TmCon_198) -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866''9839'_4 -> Any -> T_TmCon_198
MAlonzo.Code.RawU.C_tmCon_202 (T__'8866''9839'_4 -> Any
forall a b. a -> b
coe T__'8866''9839'_4
d_integer_170) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
-- VerifiedCompilation.UCaseReduce.ast₁
d_ast'8321'_178 :: MAlonzo.Code.Untyped.T__'8866'_14
d_ast'8321'_178 :: T__'8866'_14
d_ast'8321'_178
  = (T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> Any -> Any -> T__'8866'_14
forall a b. a -> b
coe
      T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
      ((Integer -> [T__'8866'_14] -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
         Integer -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_constr_34 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
         ((Any -> [Any]) -> Any -> Any
forall a b. a -> b
coe
            Any -> [Any]
MAlonzo.Code.Data.List.Base.du_'91'_'93'_286
            ((Integer -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14
du_con'45'integer_174 (Integer -> Any
forall a b. a -> b
coe (Integer
99 :: Integer)))))
      ((Any -> [Any]) -> Any -> Any
forall a b. a -> b
coe
         Any -> [Any]
MAlonzo.Code.Data.List.Base.du_'91'_'93'_286
         ((Any -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
            Any -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18
            (Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)))
-- VerifiedCompilation.UCaseReduce.ast₁'
d_ast'8321'''_180 :: MAlonzo.Code.Untyped.T__'8866'_14
d_ast'8321'''_180 :: T__'8866'_14
d_ast'8321'''_180
  = (T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> Any -> Any -> T__'8866'_14
forall a b. a -> b
coe
      T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
      ((Any -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
         Any -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18
         (Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
      ((Integer -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14
du_con'45'integer_174 (Integer -> Any
forall a b. a -> b
coe (Integer
99 :: Integer)))
-- VerifiedCompilation.UCaseReduce.ast
d_ast_184 :: MAlonzo.Code.Untyped.T__'8866'_14
d_ast_184 :: T__'8866'_14
d_ast_184
  = (T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> Any -> Any -> T__'8866'_14
forall a b. a -> b
coe
      T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
      ((Integer -> [T__'8866'_14] -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
         Integer -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_constr_34 (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
         ((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 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14
du_con'45'integer_174 (Integer -> Any
forall a b. a -> b
coe (Integer
12 :: Integer)))
            ((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 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14
du_con'45'integer_174 (Integer -> Any
forall a b. a -> b
coe (Integer
42 :: Integer)))
               ([Any] -> Any
forall a b. a -> b
coe [Any]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16))))
      ((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__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
            T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
            ((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
               T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
               ((Any -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
                  Any -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18
                  ((Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
                     Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                     (Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)))))
         ((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__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
               T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
               ((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
                  T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
                  ((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
                     T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
                     ((Integer -> [T__'8866'_14] -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                        Integer -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_constr_34 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
                        ((Any -> [Any]) -> Any -> Any
forall a b. a -> b
coe
                           Any -> [Any]
MAlonzo.Code.Data.List.Base.du_'91'_'93'_286
                           ((Integer -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14
du_con'45'integer_174 (Integer -> Any
forall a b. a -> b
coe (Integer
99 :: Integer)))))
                     ((Any -> [Any]) -> Any -> Any
forall a b. a -> b
coe
                        Any -> [Any]
MAlonzo.Code.Data.List.Base.du_'91'_'93'_286
                        ((Any -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
                           Any -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18
                           (Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))))))
            ([Any] -> Any
forall a b. a -> b
coe [Any]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)))
-- VerifiedCompilation.UCaseReduce.ast'
d_ast''_186 :: MAlonzo.Code.Untyped.T__'8866'_14
d_ast''_186 :: T__'8866'_14
d_ast''_186
  = (T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> Any -> Any -> T__'8866'_14
forall a b. a -> b
coe
      T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
      ((Integer -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14
du_con'45'integer_174 (Integer -> Any
forall a b. a -> b
coe (Integer
42 :: Integer)))
      ((Integer -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14
du_con'45'integer_174 (Integer -> Any
forall a b. a -> b
coe (Integer
99 :: Integer)))