{-# 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.Algorithmic.ReductionEC 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.Sigma
import qualified MAlonzo.Code.Algorithmic
import qualified MAlonzo.Code.Algorithmic.CEK
import qualified MAlonzo.Code.Builtin
import qualified MAlonzo.Code.Builtin.Signature
import qualified MAlonzo.Code.Data.Fin.Base
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.List.NonEmpty.Base
import qualified MAlonzo.Code.Data.Vec.Base
import qualified MAlonzo.Code.Type
import qualified MAlonzo.Code.Type.BetaNBE
import qualified MAlonzo.Code.Type.BetaNormal
import qualified MAlonzo.Code.Utils
import qualified MAlonzo.Code.Utils.List

-- Algorithmic.ReductionEC._.SigTy
d_SigTy_6 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> ()
d_SigTy_6 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 p
a9 = ()
-- Algorithmic.ReductionEC._.sig2SigTy
d_sig2SigTy_12 ::
  MAlonzo.Code.Builtin.Signature.T_Sig_68 ->
  MAlonzo.Code.Builtin.Signature.T_SigTy_260
d_sig2SigTy_12 :: T_Sig_68 -> T_SigTy_260
d_sig2SigTy_12
  = ((T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
 -> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
 -> (T_Ctx'8902'_2 -> Any -> Any)
 -> (T_Ctx'8902'_2 -> Any -> Any -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
 -> T_Sig_68
 -> T_SigTy_260)
-> (Any -> Any -> Any -> Any)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> (Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_Sig_68
-> T_SigTy_260
forall a b. a -> b
coe
      (T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> T_Sig_68
-> T_SigTy_260
MAlonzo.Code.Builtin.Signature.du_sig2SigTy_392
      (\ Any
v0 Any
v1 Any
v2 -> (T__'8866'Ne'8902'__6 -> T__'8866'Nf'8902'__4) -> Any -> Any
forall a b. a -> b
coe T__'8866'Ne'8902'__6 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_ne_20 Any
v2)
      ((Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v0 Any
v1 Any
v2 Any
v3 -> (T__'8715''8902'__14 -> T__'8866'Ne'8902'__6) -> Any -> Any
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8866'Ne'8902'__6
MAlonzo.Code.Type.BetaNormal.C_'96'_8 Any
v3))
      (\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 ->
         (T_Kind_476
 -> T__'8866'Ne'8902'__6
 -> T__'8866'Nf'8902'__4
 -> T__'8866'Ne'8902'__6)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Kind_476
-> T__'8866'Ne'8902'__6
-> T__'8866'Nf'8902'__4
-> T__'8866'Ne'8902'__6
MAlonzo.Code.Type.BetaNormal.C__'183'__10 Any
v1 Any
v3 Any
v4)
      ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 -> (T_TyCon_6 -> T__'8866'Ne'8902'__6) -> Any
forall a b. a -> b
coe T_TyCon_6 -> T__'8866'Ne'8902'__6
MAlonzo.Code.Type.BetaNormal.C_'94'_12))
      (\ Any
v0 Any
v1 -> (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4) -> Any -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_con_22 Any
v1)
      (\ Any
v0 Any
v1 Any
v2 ->
         (T__'8866'Nf'8902'__4
 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4)
-> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C__'8658'__16 Any
v1 Any
v2)
      (\ Any
v0 Any
v1 Any
v2 -> (T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_Π_14 Any
v1 Any
v2)
-- Algorithmic.ReductionEC._.sig2type
d_sig2type_14 ::
  MAlonzo.Code.Builtin.Signature.T_Sig_68 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
d_sig2type_14 :: T_Sig_68 -> T__'8866'Nf'8902'__4
d_sig2type_14
  = ((T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
 -> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
 -> (T_Ctx'8902'_2 -> Any -> Any)
 -> (T_Ctx'8902'_2 -> Any -> Any -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
 -> T_Sig_68
 -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> (Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_Sig_68
-> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
      (T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> T_Sig_68
-> Any
MAlonzo.Code.Builtin.Signature.du_sig2type_236
      (\ Any
v0 Any
v1 Any
v2 -> (T__'8866'Ne'8902'__6 -> T__'8866'Nf'8902'__4) -> Any -> Any
forall a b. a -> b
coe T__'8866'Ne'8902'__6 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_ne_20 Any
v2)
      ((Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v0 Any
v1 Any
v2 Any
v3 -> (T__'8715''8902'__14 -> T__'8866'Ne'8902'__6) -> Any -> Any
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8866'Ne'8902'__6
MAlonzo.Code.Type.BetaNormal.C_'96'_8 Any
v3))
      (\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 ->
         (T_Kind_476
 -> T__'8866'Ne'8902'__6
 -> T__'8866'Nf'8902'__4
 -> T__'8866'Ne'8902'__6)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Kind_476
-> T__'8866'Ne'8902'__6
-> T__'8866'Nf'8902'__4
-> T__'8866'Ne'8902'__6
MAlonzo.Code.Type.BetaNormal.C__'183'__10 Any
v1 Any
v3 Any
v4)
      ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 -> (T_TyCon_6 -> T__'8866'Ne'8902'__6) -> Any
forall a b. a -> b
coe T_TyCon_6 -> T__'8866'Ne'8902'__6
MAlonzo.Code.Type.BetaNormal.C_'94'_12))
      (\ Any
v0 Any
v1 -> (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4) -> Any -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_con_22 Any
v1)
      (\ Any
v0 Any
v1 Any
v2 ->
         (T__'8866'Nf'8902'__4
 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4)
-> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C__'8658'__16 Any
v1 Any
v2)
      (\ Any
v0 Any
v1 Any
v2 -> (T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_Π_14 Any
v1 Any
v2)
-- Algorithmic.ReductionEC.Value
d_Value_28 :: p -> p -> ()
d_Value_28 p
a0 p
a1 = ()
data T_Value_28
  = C_V'45'ƛ_138 | C_V'45'Λ_146 | C_V'45'wrap_156 T_Value_28 |
    C_V'45'con_162 |
    C_V'45'I'8658'_184 MAlonzo.Code.Builtin.T_Builtin_2 Integer
                       MAlonzo.Code.Utils.T__'8724'_'8803'__120 Integer Integer
                       MAlonzo.Code.Utils.T__'8724'_'8803'__120
                       MAlonzo.Code.Builtin.Signature.T_SigTy_260 T_BApp_74 |
    C_V'45'IΠ_208 MAlonzo.Code.Builtin.T_Builtin_2 Integer Integer
                  MAlonzo.Code.Utils.T__'8724'_'8803'__120 Integer Integer
                  MAlonzo.Code.Utils.T__'8724'_'8803'__120
                  MAlonzo.Code.Builtin.Signature.T_SigTy_260 T_BApp_74 |
    C_V'45'constr_234 MAlonzo.Code.Utils.List.T_Bwd_6
                      MAlonzo.Code.Utils.List.T_IBwd_396
                      MAlonzo.Code.Utils.List.T_IIBwd_832
-- Algorithmic.ReductionEC.VList
d_VList_34 ::
  MAlonzo.Code.Utils.List.T_Bwd_6 ->
  MAlonzo.Code.Utils.List.T_IBwd_396 -> ()
d_VList_34 :: T_Bwd_6 -> T_IBwd_396 -> ()
d_VList_34 = T_Bwd_6 -> T_IBwd_396 -> ()
forall a. a
erased
-- Algorithmic.ReductionEC.deval
d_deval_40 ::
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  T_Value_28 -> MAlonzo.Code.Algorithmic.T__'8866'__168
d_deval_40 :: T__'8866'Nf'8902'__4
-> T__'8866'__168 -> T_Value_28 -> T__'8866'__168
d_deval_40 ~T__'8866'Nf'8902'__4
v0 T__'8866'__168
v1 ~T_Value_28
v2 = T__'8866'__168 -> T__'8866'__168
du_deval_40 T__'8866'__168
v1
du_deval_40 ::
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168
du_deval_40 :: T__'8866'__168 -> T__'8866'__168
du_deval_40 T__'8866'__168
v0 = T__'8866'__168 -> T__'8866'__168
forall a b. a -> b
coe T__'8866'__168
v0
-- Algorithmic.ReductionEC.deval-VecList
d_deval'45'VecList_48 ::
  Integer ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_24 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_24
d_deval'45'VecList_48 :: Integer -> T_Vec_24 -> T_Vec_24
d_deval'45'VecList_48 ~Integer
v0 T_Vec_24
v1 = T_Vec_24 -> T_Vec_24
du_deval'45'VecList_48 T_Vec_24
v1
du_deval'45'VecList_48 ::
  MAlonzo.Code.Data.Vec.Base.T_Vec_24 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_24
du_deval'45'VecList_48 :: T_Vec_24 -> T_Vec_24
du_deval'45'VecList_48 T_Vec_24
v0
  = case T_Vec_24 -> T_Vec_24
forall a b. a -> b
coe T_Vec_24
v0 of
      T_Vec_24
MAlonzo.Code.Data.Vec.Base.C_'91''93'_28 -> T_Vec_24 -> T_Vec_24
forall a b. a -> b
coe T_Vec_24
v0
      MAlonzo.Code.Data.Vec.Base.C__'8759'__36 Any
v2 T_Vec_24
v3
        -> (Any -> T_Vec_24 -> T_Vec_24) -> Any -> 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
             (((Any -> Any) -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                (Any -> Any) -> [Any] -> [Any]
MAlonzo.Code.Data.List.Base.du_map_22
                ((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v4 -> T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (Any -> T_Σ_14
forall a b. a -> b
coe Any
v4)))
                (Any -> Any
forall a b. a -> b
coe Any
v2))
             ((T_Vec_24 -> T_Vec_24) -> Any -> Any
forall a b. a -> b
coe T_Vec_24 -> T_Vec_24
du_deval'45'VecList_48 (T_Vec_24 -> Any
forall a b. a -> b
coe T_Vec_24
v3))
      T_Vec_24
_ -> T_Vec_24
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algorithmic.ReductionEC.BApp
d_BApp_74 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> ()
d_BApp_74 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 p
a9 p
a10 p
a11 = ()
data T_BApp_74
  = C_base_78 | C_step_100 T_BApp_74 T_Value_28 |
    C_step'8902'_130 MAlonzo.Code.Builtin.Signature.T_SigTy_260
                     T_BApp_74
-- Algorithmic.ReductionEC.red2cekVal
d_red2cekVal_240 ::
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  T_Value_28 -> MAlonzo.Code.Algorithmic.CEK.T_Value_52
d_red2cekVal_240 :: T__'8866'Nf'8902'__4 -> T__'8866'__168 -> T_Value_28 -> T_Value_52
d_red2cekVal_240 T__'8866'Nf'8902'__4
v0 T__'8866'__168
v1 T_Value_28
v2
  = case T_Value_28 -> T_Value_28
forall a b. a -> b
coe T_Value_28
v2 of
      T_Value_28
C_V'45'ƛ_138
        -> case T__'8866'__168 -> T__'8866'__168
forall a b. a -> b
coe T__'8866'__168
v1 of
             MAlonzo.Code.Algorithmic.C_ƛ_180 T__'8866'__168
v8
               -> (T_Ctx_2 -> T__'8866'__168 -> T_Env_26 -> T_Value_52)
-> Any -> T__'8866'__168 -> Any -> T_Value_52
forall a b. a -> b
coe
                    T_Ctx_2 -> T__'8866'__168 -> T_Env_26 -> T_Value_52
MAlonzo.Code.Algorithmic.CEK.C_V'45'ƛ_64
                    (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4) T__'8866'__168
v8
                    (T_Env_26 -> Any
forall a b. a -> b
coe T_Env_26
MAlonzo.Code.Algorithmic.CEK.C_'91''93'_202)
             T__'8866'__168
_ -> T_Value_52
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Value_28
C_V'45'Λ_146
        -> case T__'8866'__168 -> T__'8866'__168
forall a b. a -> b
coe T__'8866'__168
v1 of
             MAlonzo.Code.Algorithmic.C_Λ_192 T__'8866'__168
v8
               -> (T_Ctx_2 -> T__'8866'__168 -> T_Env_26 -> T_Value_52)
-> Any -> T__'8866'__168 -> Any -> T_Value_52
forall a b. a -> b
coe
                    T_Ctx_2 -> T__'8866'__168 -> T_Env_26 -> T_Value_52
MAlonzo.Code.Algorithmic.CEK.C_V'45'Λ_74
                    (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4) T__'8866'__168
v8
                    (T_Env_26 -> Any
forall a b. a -> b
coe T_Env_26
MAlonzo.Code.Algorithmic.CEK.C_'91''93'_202)
             T__'8866'__168
_ -> T_Value_52
forall a. a
MAlonzo.RTE.mazUnreachableError
      C_V'45'wrap_156 T_Value_28
v7
        -> case T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v0 of
             MAlonzo.Code.Type.BetaNormal.C_μ_24 T_Kind_476
v9 T__'8866'Nf'8902'__4
v10 T__'8866'Nf'8902'__4
v11
               -> case T__'8866'__168 -> T__'8866'__168
forall a b. a -> b
coe T__'8866'__168
v1 of
                    MAlonzo.Code.Algorithmic.C_wrap_210 T__'8866'__168
v15
                      -> (T_Value_52 -> T_Value_52) -> T_Value_52 -> T_Value_52
forall a b. a -> b
coe
                           T_Value_52 -> T_Value_52
MAlonzo.Code.Algorithmic.CEK.C_V'45'wrap_82
                           (T__'8866'Nf'8902'__4 -> T__'8866'__168 -> T_Value_28 -> T_Value_52
d_red2cekVal_240
                              ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866''8902'__20 -> T__'8866'Nf'8902'__4)
-> Any -> Any -> Any -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
                                 T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866''8902'__20 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNBE.d_nf_258
                                 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)
                                 ((T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> T_Kind_476 -> Any -> T__'8866''8902'__20 -> Any
forall a b. a -> b
coe
                                    T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.C__'183'__30 T_Kind_476
v9
                                    ((T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> Any -> T__'8866''8902'__20 -> Any -> Any
forall a b. a -> b
coe
                                       T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.C__'183'__30
                                       ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                                          T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9)
                                          (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478))
                                       (T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
MAlonzo.Code.Type.BetaNormal.d_embNf_128
                                          (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                          ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> Any -> Any -> T_Kind_476
forall a b. a -> b
coe
                                             T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482
                                             ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9)
                                                (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478))
                                             ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9)
                                                (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)))
                                          (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v10))
                                       ((T__'8866''8902'__20 -> T__'8866''8902'__20) -> Any -> Any
forall a b. a -> b
coe
                                          T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_ƛ_28
                                          ((T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> T_Kind_476 -> T__'8866''8902'__20 -> Any -> Any
forall a b. a -> b
coe
                                             T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.C_μ_32 T_Kind_476
v9
                                             (T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
MAlonzo.Code.Type.BetaNormal.d_embNf_128
                                                ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> Any -> Any -> T_Ctx'8902'_2
forall a b. a -> b
coe
                                                   T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6
                                                   (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9))
                                                ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> Any -> Any -> T_Kind_476
forall a b. a -> b
coe
                                                   T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482
                                                   ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                      T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9)
                                                      (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478))
                                                   ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                      T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9)
                                                      (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)))
                                                ((T_Ctx'8902'_2
 -> T_Kind_476
 -> T_Kind_476
 -> T__'8866'Nf'8902'__4
 -> T__'8866'Nf'8902'__4)
-> Any
-> Any
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
                                                   T_Ctx'8902'_2
-> T_Kind_476
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.d_weakenNf_122
                                                   (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                                   ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                      T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482
                                                      ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                         T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9)
                                                         (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478))
                                                      ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                         T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9)
                                                         (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)))
                                                   T_Kind_476
v9 T__'8866'Nf'8902'__4
v10))
                                             ((T__'8715''8902'__14 -> T__'8866''8902'__20) -> Any -> Any
forall a b. a -> b
coe
                                                T__'8715''8902'__14 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'96'_22
                                                (T__'8715''8902'__14 -> Any
forall a b. a -> b
coe T__'8715''8902'__14
MAlonzo.Code.Type.C_Z_16)))))
                                    (T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
MAlonzo.Code.Type.BetaNormal.d_embNf_128
                                       (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4) (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v9) (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v11))))
                              (T__'8866'__168 -> T__'8866'__168
forall a b. a -> b
coe T__'8866'__168
v15) (T_Value_28 -> T_Value_28
forall a b. a -> b
coe T_Value_28
v7))
                    T__'8866'__168
_ -> T_Value_52
forall a. a
MAlonzo.RTE.mazUnreachableError
             T__'8866'Nf'8902'__4
_ -> T_Value_52
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Value_28
C_V'45'con_162
        -> case T__'8866'__168 -> T__'8866'__168
forall a b. a -> b
coe T__'8866'__168
v1 of
             MAlonzo.Code.Algorithmic.C_con_248 T__'8866'Nf'8902'__4
v5 Any
v7
               -> (Any -> T_Value_52) -> Any -> T_Value_52
forall a b. a -> b
coe Any -> T_Value_52
MAlonzo.Code.Algorithmic.CEK.C_V'45'con_86 Any
v7
             T__'8866'__168
_ -> T_Value_52
forall a. a
MAlonzo.RTE.mazUnreachableError
      C_V'45'I'8658'_184 T_Builtin_2
v3 Integer
v6 T__'8724'_'8803'__120
v7 Integer
v8 Integer
v9 T__'8724'_'8803'__120
v10 T_SigTy_260
v11 T_BApp_74
v13
        -> (T_Builtin_2
 -> Integer
 -> T__'8724'_'8803'__120
 -> Integer
 -> Integer
 -> T__'8724'_'8803'__120
 -> T_SigTy_260
 -> T_BApp_48
 -> T_Value_52)
-> T_Builtin_2
-> Integer
-> T__'8724'_'8803'__120
-> Integer
-> Integer
-> T__'8724'_'8803'__120
-> T_SigTy_260
-> Any
-> T_Value_52
forall a b. a -> b
coe
             T_Builtin_2
-> Integer
-> T__'8724'_'8803'__120
-> Integer
-> Integer
-> T__'8724'_'8803'__120
-> T_SigTy_260
-> T_BApp_48
-> T_Value_52
MAlonzo.Code.Algorithmic.CEK.C_V'45'I'8658'_106 T_Builtin_2
v3 Integer
v6 T__'8724'_'8803'__120
v7 Integer
v8 Integer
v9 T__'8724'_'8803'__120
v10
             T_SigTy_260
v11 ((T__'8724'_'8803'__120
 -> T__'8724'_'8803'__120
 -> T__'8866'__168
 -> T_BApp_74
 -> T_BApp_48)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8724'_'8803'__120
-> T__'8724'_'8803'__120
-> T__'8866'__168
-> T_BApp_74
-> T_BApp_48
du_red2cekBApp_266 (T__'8724'_'8803'__120 -> Any
forall a b. a -> b
coe T__'8724'_'8803'__120
v7) (T__'8724'_'8803'__120 -> Any
forall a b. a -> b
coe T__'8724'_'8803'__120
v10) (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v1) (T_BApp_74 -> Any
forall a b. a -> b
coe T_BApp_74
v13))
      C_V'45'IΠ_208 T_Builtin_2
v3 Integer
v6 Integer
v7 T__'8724'_'8803'__120
v8 Integer
v9 Integer
v10 T__'8724'_'8803'__120
v11 T_SigTy_260
v12 T_BApp_74
v14
        -> (T_Builtin_2
 -> Integer
 -> Integer
 -> T__'8724'_'8803'__120
 -> Integer
 -> Integer
 -> T__'8724'_'8803'__120
 -> T_SigTy_260
 -> T_BApp_48
 -> T_Value_52)
-> T_Builtin_2
-> Integer
-> Integer
-> T__'8724'_'8803'__120
-> Integer
-> Integer
-> T__'8724'_'8803'__120
-> T_SigTy_260
-> Any
-> T_Value_52
forall a b. a -> b
coe
             T_Builtin_2
-> Integer
-> Integer
-> T__'8724'_'8803'__120
-> Integer
-> Integer
-> T__'8724'_'8803'__120
-> T_SigTy_260
-> T_BApp_48
-> T_Value_52
MAlonzo.Code.Algorithmic.CEK.C_V'45'IΠ_128 T_Builtin_2
v3 Integer
v6 Integer
v7 T__'8724'_'8803'__120
v8 Integer
v9 Integer
v10 T__'8724'_'8803'__120
v11
             T_SigTy_260
v12 ((T__'8724'_'8803'__120
 -> T__'8724'_'8803'__120
 -> T__'8866'__168
 -> T_BApp_74
 -> T_BApp_48)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8724'_'8803'__120
-> T__'8724'_'8803'__120
-> T__'8866'__168
-> T_BApp_74
-> T_BApp_48
du_red2cekBApp_266 (T__'8724'_'8803'__120 -> Any
forall a b. a -> b
coe T__'8724'_'8803'__120
v8) (T__'8724'_'8803'__120 -> Any
forall a b. a -> b
coe T__'8724'_'8803'__120
v11) (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v1) (T_BApp_74 -> Any
forall a b. a -> b
coe T_BApp_74
v14))
      C_V'45'constr_234 T_Bwd_6
v8 T_IBwd_396
v10 T_IIBwd_832
v11
        -> case T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v0 of
             MAlonzo.Code.Type.BetaNormal.C_SOP_28 Integer
v15 T_Vec_24
v16
               -> case T__'8866'__168 -> T__'8866'__168
forall a b. a -> b
coe T__'8866'__168
v1 of
                    MAlonzo.Code.Algorithmic.C_constr_230 T_Fin_6
v18 [T__'8866'Nf'8902'__4]
v20 T_IList_302
v22
                      -> (T_Fin_6 -> T_Bwd_6 -> T_IBwd_396 -> T_Value_52)
-> T_Fin_6 -> Any -> T_IBwd_396 -> T_Value_52
forall a b. a -> b
coe
                           T_Fin_6 -> T_Bwd_6 -> T_IBwd_396 -> T_Value_52
MAlonzo.Code.Algorithmic.CEK.C_V'45'constr_140 T_Fin_6
v18
                           ((T_Bwd_6 -> [Any] -> T_Bwd_6) -> Any -> Any -> Any
forall a b. a -> b
coe
                              T_Bwd_6 -> [Any] -> T_Bwd_6
MAlonzo.Code.Utils.List.du__'60''62''60'__54
                              (T_Bwd_6 -> Any
forall a b. a -> b
coe T_Bwd_6
MAlonzo.Code.Utils.List.C_'91''93'_10)
                              ((T_Vec_24 -> T_Fin_6 -> Any) -> Any -> Any -> Any
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
v16) (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v18)))
                           (T_Bwd_6 -> T_IBwd_396 -> T_IIBwd_832 -> T_IBwd_396
d_red2cekVal'45'VList_280
                              ((T_Bwd_6 -> [Any] -> T_Bwd_6) -> Any -> Any -> T_Bwd_6
forall a b. a -> b
coe
                                 T_Bwd_6 -> [Any] -> T_Bwd_6
MAlonzo.Code.Utils.List.du__'60''62''60'__54
                                 (T_Bwd_6 -> Any
forall a b. a -> b
coe T_Bwd_6
MAlonzo.Code.Utils.List.C_'91''93'_10)
                                 ((T_Vec_24 -> T_Fin_6 -> Any) -> Any -> Any -> Any
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
v16) (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v18)))
                              (T_IBwd_396 -> T_IBwd_396
forall a b. a -> b
coe T_IBwd_396
v10) (T_IIBwd_832 -> T_IIBwd_832
forall a b. a -> b
coe T_IIBwd_832
v11))
                    T__'8866'__168
_ -> T_Value_52
forall a. a
MAlonzo.RTE.mazUnreachableError
             T__'8866'Nf'8902'__4
_ -> T_Value_52
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Value_28
_ -> T_Value_52
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algorithmic.ReductionEC.red2cekBApp
d_red2cekBApp_266 ::
  MAlonzo.Code.Builtin.T_Builtin_2 ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Utils.T__'8724'_'8803'__120 ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Utils.T__'8724'_'8803'__120 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  MAlonzo.Code.Builtin.Signature.T_SigTy_260 ->
  T_BApp_74 -> MAlonzo.Code.Algorithmic.CEK.T_BApp_48
d_red2cekBApp_266 :: T_Builtin_2
-> Integer
-> Integer
-> Integer
-> T__'8724'_'8803'__120
-> Integer
-> Integer
-> Integer
-> T__'8724'_'8803'__120
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T_SigTy_260
-> T_BApp_74
-> T_BApp_48
d_red2cekBApp_266 ~T_Builtin_2
v0 ~Integer
v1 ~Integer
v2 ~Integer
v3 T__'8724'_'8803'__120
v4 ~Integer
v5 ~Integer
v6 ~Integer
v7 T__'8724'_'8803'__120
v8 ~T__'8866'Nf'8902'__4
v9 T__'8866'__168
v10 ~T_SigTy_260
v11
                  T_BApp_74
v12
  = T__'8724'_'8803'__120
-> T__'8724'_'8803'__120
-> T__'8866'__168
-> T_BApp_74
-> T_BApp_48
du_red2cekBApp_266 T__'8724'_'8803'__120
v4 T__'8724'_'8803'__120
v8 T__'8866'__168
v10 T_BApp_74
v12
du_red2cekBApp_266 ::
  MAlonzo.Code.Utils.T__'8724'_'8803'__120 ->
  MAlonzo.Code.Utils.T__'8724'_'8803'__120 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  T_BApp_74 -> MAlonzo.Code.Algorithmic.CEK.T_BApp_48
du_red2cekBApp_266 :: T__'8724'_'8803'__120
-> T__'8724'_'8803'__120
-> T__'8866'__168
-> T_BApp_74
-> T_BApp_48
du_red2cekBApp_266 T__'8724'_'8803'__120
v0 T__'8724'_'8803'__120
v1 T__'8866'__168
v2 T_BApp_74
v3
  = case T_BApp_74 -> T_BApp_74
forall a b. a -> b
coe T_BApp_74
v3 of
      T_BApp_74
C_base_78 -> T_BApp_48 -> T_BApp_48
forall a b. a -> b
coe T_BApp_48
MAlonzo.Code.Algorithmic.CEK.C_base_144
      C_step_100 T_BApp_74
v13 T_Value_28
v15
        -> case T__'8724'_'8803'__120 -> T__'8724'_'8803'__120
forall a b. a -> b
coe T__'8724'_'8803'__120
v1 of
             MAlonzo.Code.Utils.C_bubble_132 T__'8724'_'8803'__120
v19
               -> case T__'8866'__168 -> T__'8866'__168
forall a b. a -> b
coe T__'8866'__168
v2 of
                    MAlonzo.Code.Algorithmic.C__'183'__186 T__'8866'Nf'8902'__4
v20 T__'8866'__168
v22 T__'8866'__168
v23
                      -> (T__'8866'Nf'8902'__4 -> T_BApp_48 -> T_Value_52 -> T_BApp_48)
-> T__'8866'Nf'8902'__4 -> Any -> T_Value_52 -> T_BApp_48
forall a b. a -> b
coe
                           T__'8866'Nf'8902'__4 -> T_BApp_48 -> T_Value_52 -> T_BApp_48
MAlonzo.Code.Algorithmic.CEK.C__'36'__162 T__'8866'Nf'8902'__4
v20
                           ((T__'8724'_'8803'__120
 -> T__'8724'_'8803'__120
 -> T__'8866'__168
 -> T_BApp_74
 -> T_BApp_48)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8724'_'8803'__120
-> T__'8724'_'8803'__120
-> T__'8866'__168
-> T_BApp_74
-> T_BApp_48
du_red2cekBApp_266 (T__'8724'_'8803'__120 -> Any
forall a b. a -> b
coe T__'8724'_'8803'__120
v0) (T__'8724'_'8803'__120 -> Any
forall a b. a -> b
coe T__'8724'_'8803'__120
v19) (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v22) (T_BApp_74 -> Any
forall a b. a -> b
coe T_BApp_74
v13))
                           (T__'8866'Nf'8902'__4 -> T__'8866'__168 -> T_Value_28 -> T_Value_52
d_red2cekVal_240 (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v20) (T__'8866'__168 -> T__'8866'__168
forall a b. a -> b
coe T__'8866'__168
v23) (T_Value_28 -> T_Value_28
forall a b. a -> b
coe T_Value_28
v15))
                    T__'8866'__168
_ -> T_BApp_48
forall a. a
MAlonzo.RTE.mazUnreachableError
             T__'8724'_'8803'__120
_ -> T_BApp_48
forall a. a
MAlonzo.RTE.mazUnreachableError
      C_step'8902'_130 T_SigTy_260
v13 T_BApp_74
v15
        -> case T__'8724'_'8803'__120 -> T__'8724'_'8803'__120
forall a b. a -> b
coe T__'8724'_'8803'__120
v0 of
             MAlonzo.Code.Utils.C_bubble_132 T__'8724'_'8803'__120
v22
               -> case T__'8866'__168 -> T__'8866'__168
forall a b. a -> b
coe T__'8866'__168
v2 of
                    MAlonzo.Code.Algorithmic.C__'183''8902'_'47'__202 T_Kind_476
v23 T__'8866'Nf'8902'__4
v25 T__'8866'__168
v26 T__'8866'Nf'8902'__4
v27
                      -> (T_Kind_476
 -> T__'8866'Nf'8902'__4
 -> T_SigTy_260
 -> T_BApp_48
 -> T__'8866'Nf'8902'__4
 -> T_BApp_48)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T_SigTy_260
-> Any
-> T__'8866'Nf'8902'__4
-> T_BApp_48
forall a b. a -> b
coe
                           T_Kind_476
-> T__'8866'Nf'8902'__4
-> T_SigTy_260
-> T_BApp_48
-> T__'8866'Nf'8902'__4
-> T_BApp_48
MAlonzo.Code.Algorithmic.CEK.C__'36''36'__190 T_Kind_476
v23 T__'8866'Nf'8902'__4
v25 T_SigTy_260
v13
                           ((T__'8724'_'8803'__120
 -> T__'8724'_'8803'__120
 -> T__'8866'__168
 -> T_BApp_74
 -> T_BApp_48)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8724'_'8803'__120
-> T__'8724'_'8803'__120
-> T__'8866'__168
-> T_BApp_74
-> T_BApp_48
du_red2cekBApp_266 (T__'8724'_'8803'__120 -> Any
forall a b. a -> b
coe T__'8724'_'8803'__120
v22) (T__'8724'_'8803'__120 -> Any
forall a b. a -> b
coe T__'8724'_'8803'__120
v1) (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v26) (T_BApp_74 -> Any
forall a b. a -> b
coe T_BApp_74
v15)) T__'8866'Nf'8902'__4
v27
                    T__'8866'__168
_ -> T_BApp_48
forall a. a
MAlonzo.RTE.mazUnreachableError
             T__'8724'_'8803'__120
_ -> T_BApp_48
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_BApp_74
_ -> T_BApp_48
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algorithmic.ReductionEC.red2cekVal-VList
d_red2cekVal'45'VList_280 ::
  MAlonzo.Code.Utils.List.T_Bwd_6 ->
  MAlonzo.Code.Utils.List.T_IBwd_396 ->
  MAlonzo.Code.Utils.List.T_IIBwd_832 ->
  MAlonzo.Code.Utils.List.T_IBwd_396
d_red2cekVal'45'VList_280 :: T_Bwd_6 -> T_IBwd_396 -> T_IIBwd_832 -> T_IBwd_396
d_red2cekVal'45'VList_280 T_Bwd_6
v0 T_IBwd_396
v1 T_IIBwd_832
v2
  = case T_IIBwd_832 -> T_IIBwd_832
forall a b. a -> b
coe T_IIBwd_832
v2 of
      T_IIBwd_832
MAlonzo.Code.Utils.List.C_'91''93'_840
        -> T_IBwd_396 -> T_IBwd_396
forall a b. a -> b
coe T_IBwd_396
MAlonzo.Code.Utils.List.C_'91''93'_402
      MAlonzo.Code.Utils.List.C__'58''60'__850 T_IIBwd_832
v7 Any
v8
        -> case T_Bwd_6 -> T_Bwd_6
forall a b. a -> b
coe T_Bwd_6
v0 of
             MAlonzo.Code.Utils.List.C__'58''60'__12 T_Bwd_6
v9 Any
v10
               -> case T_IBwd_396 -> T_IBwd_396
forall a b. a -> b
coe T_IBwd_396
v1 of
                    MAlonzo.Code.Utils.List.C__'58''60'__408 T_IBwd_396
v13 Any
v14
                      -> (T_IBwd_396 -> Any -> T_IBwd_396)
-> T_IBwd_396 -> T_Value_52 -> T_IBwd_396
forall a b. a -> b
coe
                           T_IBwd_396 -> Any -> T_IBwd_396
MAlonzo.Code.Utils.List.C__'58''60'__408
                           (T_Bwd_6 -> T_IBwd_396 -> T_IIBwd_832 -> T_IBwd_396
d_red2cekVal'45'VList_280 (T_Bwd_6 -> T_Bwd_6
forall a b. a -> b
coe T_Bwd_6
v9) (T_IBwd_396 -> T_IBwd_396
forall a b. a -> b
coe T_IBwd_396
v13) (T_IIBwd_832 -> T_IIBwd_832
forall a b. a -> b
coe T_IIBwd_832
v7))
                           (T__'8866'Nf'8902'__4 -> T__'8866'__168 -> T_Value_28 -> T_Value_52
d_red2cekVal_240 (Any -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe Any
v10) (Any -> T__'8866'__168
forall a b. a -> b
coe Any
v14) (Any -> T_Value_28
forall a b. a -> b
coe Any
v8))
                    T_IBwd_396
_ -> T_IBwd_396
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_Bwd_6
_ -> T_IBwd_396
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_IIBwd_832
_ -> T_IBwd_396
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algorithmic.ReductionEC.BUILTIN'
d_BUILTIN''_326 ::
  MAlonzo.Code.Builtin.T_Builtin_2 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  Integer ->
  MAlonzo.Code.Utils.T__'8724'_'8803'__120 ->
  Integer ->
  MAlonzo.Code.Utils.T__'8724'_'8803'__120 ->
  MAlonzo.Code.Builtin.Signature.T_SigTy_260 ->
  T_BApp_74 -> MAlonzo.Code.Algorithmic.T__'8866'__168
d_BUILTIN''_326 :: T_Builtin_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> Integer
-> T__'8724'_'8803'__120
-> Integer
-> T__'8724'_'8803'__120
-> T_SigTy_260
-> T_BApp_74
-> T__'8866'__168
d_BUILTIN''_326 T_Builtin_2
v0 T__'8866'Nf'8902'__4
v1 T__'8866'__168
v2 ~Integer
v3 T__'8724'_'8803'__120
v4 ~Integer
v5 T__'8724'_'8803'__120
v6 ~T_SigTy_260
v7 T_BApp_74
v8
  = T_Builtin_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8724'_'8803'__120
-> T__'8724'_'8803'__120
-> T_BApp_74
-> T__'8866'__168
du_BUILTIN''_326 T_Builtin_2
v0 T__'8866'Nf'8902'__4
v1 T__'8866'__168
v2 T__'8724'_'8803'__120
v4 T__'8724'_'8803'__120
v6 T_BApp_74
v8
du_BUILTIN''_326 ::
  MAlonzo.Code.Builtin.T_Builtin_2 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  MAlonzo.Code.Utils.T__'8724'_'8803'__120 ->
  MAlonzo.Code.Utils.T__'8724'_'8803'__120 ->
  T_BApp_74 -> MAlonzo.Code.Algorithmic.T__'8866'__168
du_BUILTIN''_326 :: T_Builtin_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8724'_'8803'__120
-> T__'8724'_'8803'__120
-> T_BApp_74
-> T__'8866'__168
du_BUILTIN''_326 T_Builtin_2
v0 T__'8866'Nf'8902'__4
v1 T__'8866'__168
v2 T__'8724'_'8803'__120
v3 T__'8724'_'8803'__120
v4 T_BApp_74
v5
  = (T_Builtin_2
 -> T__'8866'Nf'8902'__4 -> T_BApp_48 -> T__'8866'__168)
-> Any -> Any -> Any -> T__'8866'__168
forall a b. a -> b
coe
      T_Builtin_2 -> T__'8866'Nf'8902'__4 -> T_BApp_48 -> T__'8866'__168
MAlonzo.Code.Algorithmic.CEK.du_BUILTIN''_980 (T_Builtin_2 -> Any
forall a b. a -> b
coe T_Builtin_2
v0) (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v1)
      ((T__'8724'_'8803'__120
 -> T__'8724'_'8803'__120
 -> T__'8866'__168
 -> T_BApp_74
 -> T_BApp_48)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8724'_'8803'__120
-> T__'8724'_'8803'__120
-> T__'8866'__168
-> T_BApp_74
-> T_BApp_48
du_red2cekBApp_266 (T__'8724'_'8803'__120 -> Any
forall a b. a -> b
coe T__'8724'_'8803'__120
v3) (T__'8724'_'8803'__120 -> Any
forall a b. a -> b
coe T__'8724'_'8803'__120
v4) (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v2) (T_BApp_74 -> Any
forall a b. a -> b
coe T_BApp_74
v5))
-- Algorithmic.ReductionEC.Error
d_Error_338 :: p -> p -> p -> p -> ()
d_Error_338 p
a0 p
a1 p
a2 p
a3 = ()
data T_Error_338 = C_E'45'error_346
-- Algorithmic.ReductionEC.Frame
d_Frame_352 :: p -> p -> ()
d_Frame_352 p
a0 p
a1 = ()
data T_Frame_352
  = C_'45''183'__358 MAlonzo.Code.Algorithmic.T__'8866'__168 |
    C_'45''183'v_366 MAlonzo.Code.Algorithmic.T__'8866'__168
                     T_Value_28 |
    C__'183''45'_374 MAlonzo.Code.Algorithmic.T__'8866'__168
                     T_Value_28 |
    C_'45''183''8902'_382 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 |
    C_wrap'45'_390 | C_unwrap'45'_398 |
    C_constr'45'_420 MAlonzo.Code.Utils.List.T_Bwd_6
                     [MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4]
                     MAlonzo.Code.Data.Fin.Base.T_Fin_6
                     [MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4]
                     MAlonzo.Code.Utils.List.T__'8803'_'60''62''62'__684
                     MAlonzo.Code.Utils.List.T_IBwd_396
                     MAlonzo.Code.Utils.List.T_IIBwd_832
                     MAlonzo.Code.Utils.List.T_IList_302 |
    C_case'45'_428 MAlonzo.Code.Algorithmic.T_Cases_162
-- Algorithmic.ReductionEC._[_]ᶠ
d__'91'_'93''7584'_434 ::
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  T_Frame_352 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168
d__'91'_'93''7584'_434 :: T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T_Frame_352
-> T__'8866'__168
-> T__'8866'__168
d__'91'_'93''7584'_434 T__'8866'Nf'8902'__4
v0 ~T__'8866'Nf'8902'__4
v1 T_Frame_352
v2 T__'8866'__168
v3
  = T__'8866'Nf'8902'__4
-> T_Frame_352 -> T__'8866'__168 -> T__'8866'__168
du__'91'_'93''7584'_434 T__'8866'Nf'8902'__4
v0 T_Frame_352
v2 T__'8866'__168
v3
du__'91'_'93''7584'_434 ::
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  T_Frame_352 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168
du__'91'_'93''7584'_434 :: T__'8866'Nf'8902'__4
-> T_Frame_352 -> T__'8866'__168 -> T__'8866'__168
du__'91'_'93''7584'_434 T__'8866'Nf'8902'__4
v0 T_Frame_352
v1 T__'8866'__168
v2
  = case T_Frame_352 -> T_Frame_352
forall a b. a -> b
coe T_Frame_352
v1 of
      C_'45''183'__358 T__'8866'__168
v5
        -> case T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v0 of
             MAlonzo.Code.Type.BetaNormal.C__'8658'__16 T__'8866'Nf'8902'__4
v7 T__'8866'Nf'8902'__4
v8
               -> (T__'8866'Nf'8902'__4
 -> T__'8866'__168 -> T__'8866'__168 -> T__'8866'__168)
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'__168
-> T__'8866'__168
forall a b. a -> b
coe T__'8866'Nf'8902'__4
-> T__'8866'__168 -> T__'8866'__168 -> T__'8866'__168
MAlonzo.Code.Algorithmic.C__'183'__186 T__'8866'Nf'8902'__4
v7 T__'8866'__168
v2 T__'8866'__168
v5
             T__'8866'Nf'8902'__4
_ -> T__'8866'__168
forall a. a
MAlonzo.RTE.mazUnreachableError
      C_'45''183'v_366 T__'8866'__168
v5 T_Value_28
v6
        -> case T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v0 of
             MAlonzo.Code.Type.BetaNormal.C__'8658'__16 T__'8866'Nf'8902'__4
v8 T__'8866'Nf'8902'__4
v9
               -> (T__'8866'Nf'8902'__4
 -> T__'8866'__168 -> T__'8866'__168 -> T__'8866'__168)
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'__168
-> T__'8866'__168
forall a b. a -> b
coe T__'8866'Nf'8902'__4
-> T__'8866'__168 -> T__'8866'__168 -> T__'8866'__168
MAlonzo.Code.Algorithmic.C__'183'__186 T__'8866'Nf'8902'__4
v8 T__'8866'__168
v2 T__'8866'__168
v5
             T__'8866'Nf'8902'__4
_ -> T__'8866'__168
forall a. a
MAlonzo.RTE.mazUnreachableError
      C__'183''45'_374 T__'8866'__168
v5 T_Value_28
v6
        -> (T__'8866'Nf'8902'__4
 -> T__'8866'__168 -> T__'8866'__168 -> T__'8866'__168)
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'__168
-> T__'8866'__168
forall a b. a -> b
coe T__'8866'Nf'8902'__4
-> T__'8866'__168 -> T__'8866'__168 -> T__'8866'__168
MAlonzo.Code.Algorithmic.C__'183'__186 T__'8866'Nf'8902'__4
v0 T__'8866'__168
v5 T__'8866'__168
v2
      C_'45''183''8902'_382 T__'8866'Nf'8902'__4
v5
        -> case T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v0 of
             MAlonzo.Code.Type.BetaNormal.C_Π_14 T_Kind_476
v7 T__'8866'Nf'8902'__4
v8
               -> (T_Kind_476
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
forall a b. a -> b
coe
                    T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
MAlonzo.Code.Algorithmic.C__'183''8902'_'47'__202 T_Kind_476
v7 T__'8866'Nf'8902'__4
v8 T__'8866'__168
v2 T__'8866'Nf'8902'__4
v5
             T__'8866'Nf'8902'__4
_ -> T__'8866'__168
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Frame_352
C_wrap'45'_390 -> (T__'8866'__168 -> T__'8866'__168)
-> T__'8866'__168 -> T__'8866'__168
forall a b. a -> b
coe T__'8866'__168 -> T__'8866'__168
MAlonzo.Code.Algorithmic.C_wrap_210 T__'8866'__168
v2
      T_Frame_352
C_unwrap'45'_398
        -> case T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v0 of
             MAlonzo.Code.Type.BetaNormal.C_μ_24 T_Kind_476
v7 T__'8866'Nf'8902'__4
v8 T__'8866'Nf'8902'__4
v9
               -> (T_Kind_476
 -> T__'8866'Nf'8902'__4
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> T__'8866'__168)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'__168
forall a b. a -> b
coe T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'__168
MAlonzo.Code.Algorithmic.C_unwrap_220 T_Kind_476
v7 T__'8866'Nf'8902'__4
v8 T__'8866'Nf'8902'__4
v9 T__'8866'__168
v2
             T__'8866'Nf'8902'__4
_ -> T__'8866'__168
forall a. a
MAlonzo.RTE.mazUnreachableError
      C_constr'45'_420 T_Bwd_6
v4 [T__'8866'Nf'8902'__4]
v6 T_Fin_6
v7 [T__'8866'Nf'8902'__4]
v9 T__'8803'_'60''62''62'__684
v11 T_IBwd_396
v12 T_IIBwd_832
v13 T_IList_302
v14
        -> (T_Fin_6
 -> [T__'8866'Nf'8902'__4] -> T_IList_302 -> T__'8866'__168)
-> T_Fin_6 -> Any -> Any -> T__'8866'__168
forall a b. a -> b
coe
             T_Fin_6 -> [T__'8866'Nf'8902'__4] -> T_IList_302 -> T__'8866'__168
MAlonzo.Code.Algorithmic.C_constr_230 T_Fin_6
v7
             ((T_Bwd_6 -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                T_Bwd_6 -> [Any] -> [Any]
MAlonzo.Code.Utils.List.du__'60''62''62'__42 (T_Bwd_6 -> Any
forall a b. a -> b
coe T_Bwd_6
v4)
                ((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'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v0) ([T__'8866'Nf'8902'__4] -> Any
forall a b. a -> b
coe [T__'8866'Nf'8902'__4]
v6)))
             ((T_Bwd_6 -> T_IBwd_396 -> T_IList_302 -> T_IList_302)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_Bwd_6 -> T_IBwd_396 -> T_IList_302 -> T_IList_302
MAlonzo.Code.Utils.List.du__'60''62''62'I__418 (T_Bwd_6 -> Any
forall a b. a -> b
coe T_Bwd_6
v4) (T_IBwd_396 -> Any
forall a b. a -> b
coe T_IBwd_396
v12)
                ((Any -> T_IList_302 -> T_IList_302)
-> T__'8866'__168 -> T_IList_302 -> Any
forall a b. a -> b
coe Any -> T_IList_302 -> T_IList_302
MAlonzo.Code.Utils.List.C__'8759'__314 T__'8866'__168
v2 T_IList_302
v14))
      C_case'45'_428 T_Cases_162
v6
        -> case T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v0 of
             MAlonzo.Code.Type.BetaNormal.C_SOP_28 Integer
v8 T_Vec_24
v9
               -> (Integer
 -> T_Vec_24 -> T__'8866'__168 -> T_Cases_162 -> T__'8866'__168)
-> Integer
-> T_Vec_24
-> T__'8866'__168
-> T_Cases_162
-> T__'8866'__168
forall a b. a -> b
coe Integer
-> T_Vec_24 -> T__'8866'__168 -> T_Cases_162 -> T__'8866'__168
MAlonzo.Code.Algorithmic.C_case_242 Integer
v8 T_Vec_24
v9 T__'8866'__168
v2 T_Cases_162
v6
             T__'8866'Nf'8902'__4
_ -> T__'8866'__168
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Frame_352
_ -> T__'8866'__168
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algorithmic.ReductionEC.EC
d_EC_476 :: p -> p -> ()
d_EC_476 p
a0 p
a1 = ()
data T_EC_476
  = C_'91''93'_480 |
    C__l'183'__490 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
                   T_EC_476 MAlonzo.Code.Algorithmic.T__'8866'__168 |
    C__'183'r__500 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
                   MAlonzo.Code.Algorithmic.T__'8866'__168 T_Value_28 T_EC_476 |
    C__'183''8902'_'47'__512 MAlonzo.Code.Utils.T_Kind_476
                             MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 T_EC_476
                             MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 |
    C_wrap_522 T_EC_476 |
    C_unwrap_'47'__534 MAlonzo.Code.Utils.T_Kind_476
                       MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
                       MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 T_EC_476 |
    C_constr_558 MAlonzo.Code.Utils.List.T_Bwd_6
                 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
                 [MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4]
                 MAlonzo.Code.Data.Fin.Base.T_Fin_6
                 [MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4]
                 MAlonzo.Code.Utils.List.T__'8803'_'60''62''62'__684
                 MAlonzo.Code.Utils.List.T_IBwd_396
                 MAlonzo.Code.Utils.List.T_IIBwd_832
                 MAlonzo.Code.Utils.List.T_IList_302 T_EC_476 |
    C_case_568 Integer MAlonzo.Code.Data.Vec.Base.T_Vec_24
               MAlonzo.Code.Algorithmic.T_Cases_162 T_EC_476
-- Algorithmic.ReductionEC._[_]ᴱ
d__'91'_'93''7473'_574 ::
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  T_EC_476 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168
d__'91'_'93''7473'_574 :: T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T_EC_476
-> T__'8866'__168
-> T__'8866'__168
d__'91'_'93''7473'_574 ~T__'8866'Nf'8902'__4
v0 T__'8866'Nf'8902'__4
v1 T_EC_476
v2 T__'8866'__168
v3
  = T__'8866'Nf'8902'__4
-> T_EC_476 -> T__'8866'__168 -> T__'8866'__168
du__'91'_'93''7473'_574 T__'8866'Nf'8902'__4
v1 T_EC_476
v2 T__'8866'__168
v3
du__'91'_'93''7473'_574 ::
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  T_EC_476 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168
du__'91'_'93''7473'_574 :: T__'8866'Nf'8902'__4
-> T_EC_476 -> T__'8866'__168 -> T__'8866'__168
du__'91'_'93''7473'_574 T__'8866'Nf'8902'__4
v0 T_EC_476
v1 T__'8866'__168
v2
  = case T_EC_476 -> T_EC_476
forall a b. a -> b
coe T_EC_476
v1 of
      T_EC_476
C_'91''93'_480 -> T__'8866'__168 -> T__'8866'__168
forall a b. a -> b
coe T__'8866'__168
v2
      C__l'183'__490 T__'8866'Nf'8902'__4
v3 T_EC_476
v6 T__'8866'__168
v7
        -> (T__'8866'Nf'8902'__4
 -> T__'8866'__168 -> T__'8866'__168 -> T__'8866'__168)
-> T__'8866'Nf'8902'__4 -> Any -> T__'8866'__168 -> T__'8866'__168
forall a b. a -> b
coe
             T__'8866'Nf'8902'__4
-> T__'8866'__168 -> T__'8866'__168 -> T__'8866'__168
MAlonzo.Code.Algorithmic.C__'183'__186 T__'8866'Nf'8902'__4
v3
             ((T__'8866'Nf'8902'__4
 -> T_EC_476 -> T__'8866'__168 -> T__'8866'__168)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T__'8866'Nf'8902'__4
-> T_EC_476 -> T__'8866'__168 -> T__'8866'__168
du__'91'_'93''7473'_574
                ((T__'8866'Nf'8902'__4
 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4)
-> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C__'8658'__16 T__'8866'Nf'8902'__4
v3 T__'8866'Nf'8902'__4
v0) (T_EC_476 -> Any
forall a b. a -> b
coe T_EC_476
v6)
                (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v2))
             T__'8866'__168
v7
      C__'183'r__500 T__'8866'Nf'8902'__4
v3 T__'8866'__168
v6 T_Value_28
v7 T_EC_476
v8
        -> (T__'8866'Nf'8902'__4
 -> T__'8866'__168 -> T__'8866'__168 -> T__'8866'__168)
-> T__'8866'Nf'8902'__4 -> T__'8866'__168 -> Any -> T__'8866'__168
forall a b. a -> b
coe
             T__'8866'Nf'8902'__4
-> T__'8866'__168 -> T__'8866'__168 -> T__'8866'__168
MAlonzo.Code.Algorithmic.C__'183'__186 T__'8866'Nf'8902'__4
v3 T__'8866'__168
v6
             ((T__'8866'Nf'8902'__4
 -> T_EC_476 -> T__'8866'__168 -> T__'8866'__168)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
-> T_EC_476 -> T__'8866'__168 -> T__'8866'__168
du__'91'_'93''7473'_574 (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v3) (T_EC_476 -> Any
forall a b. a -> b
coe T_EC_476
v8) (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v2))
      C__'183''8902'_'47'__512 T_Kind_476
v3 T__'8866'Nf'8902'__4
v4 T_EC_476
v7 T__'8866'Nf'8902'__4
v8
        -> (T_Kind_476
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> Any
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
forall a b. a -> b
coe
             T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
MAlonzo.Code.Algorithmic.C__'183''8902'_'47'__202 T_Kind_476
v3 T__'8866'Nf'8902'__4
v4
             ((T__'8866'Nf'8902'__4
 -> T_EC_476 -> T__'8866'__168 -> T__'8866'__168)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T__'8866'Nf'8902'__4
-> T_EC_476 -> T__'8866'__168 -> T__'8866'__168
du__'91'_'93''7473'_574
                ((T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4)
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_Π_14 T_Kind_476
v3 T__'8866'Nf'8902'__4
v4) (T_EC_476 -> Any
forall a b. a -> b
coe T_EC_476
v7) (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v2))
             T__'8866'Nf'8902'__4
v8
      C_wrap_522 T_EC_476
v7
        -> case T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v0 of
             MAlonzo.Code.Type.BetaNormal.C_μ_24 T_Kind_476
v9 T__'8866'Nf'8902'__4
v10 T__'8866'Nf'8902'__4
v11
               -> (T__'8866'__168 -> T__'8866'__168) -> Any -> T__'8866'__168
forall a b. a -> b
coe
                    T__'8866'__168 -> T__'8866'__168
MAlonzo.Code.Algorithmic.C_wrap_210
                    ((T__'8866'Nf'8902'__4
 -> T_EC_476 -> T__'8866'__168 -> T__'8866'__168)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                       T__'8866'Nf'8902'__4
-> T_EC_476 -> T__'8866'__168 -> T__'8866'__168
du__'91'_'93''7473'_574
                       ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866''8902'__20 -> T__'8866'Nf'8902'__4)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                          T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866''8902'__20 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNBE.d_nf_258
                          (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                          (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)
                          ((T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> T_Kind_476 -> Any -> T__'8866''8902'__20 -> Any
forall a b. a -> b
coe
                             T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.C__'183'__30 T_Kind_476
v9
                             ((T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> Any -> T__'8866''8902'__20 -> Any -> Any
forall a b. a -> b
coe
                                T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.C__'183'__30
                                ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                                   T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9)
                                   (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478))
                                (T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
MAlonzo.Code.Type.BetaNormal.d_embNf_128
                                   (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                   ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> Any -> Any -> T_Kind_476
forall a b. a -> b
coe
                                      T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482
                                      ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                                         T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9)
                                         (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478))
                                      ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                                         T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9)
                                         (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)))
                                   (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v10))
                                ((T__'8866''8902'__20 -> T__'8866''8902'__20) -> Any -> Any
forall a b. a -> b
coe
                                   T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_ƛ_28
                                   ((T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> T_Kind_476 -> T__'8866''8902'__20 -> Any -> Any
forall a b. a -> b
coe
                                      T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.C_μ_32 T_Kind_476
v9
                                      (T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
MAlonzo.Code.Type.BetaNormal.d_embNf_128
                                         ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> Any -> Any -> T_Ctx'8902'_2
forall a b. a -> b
coe
                                            T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6
                                            (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9))
                                         ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> Any -> Any -> T_Kind_476
forall a b. a -> b
coe
                                            T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482
                                            ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                                               T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9)
                                               (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478))
                                            ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                                               T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9)
                                               (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)))
                                         ((T_Ctx'8902'_2
 -> T_Kind_476
 -> T_Kind_476
 -> T__'8866'Nf'8902'__4
 -> T__'8866'Nf'8902'__4)
-> Any
-> Any
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
                                            T_Ctx'8902'_2
-> T_Kind_476
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.d_weakenNf_122
                                            (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                            ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                                               T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482
                                               ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                  T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9)
                                                  (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478))
                                               ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                  T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9)
                                                  (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)))
                                            T_Kind_476
v9 T__'8866'Nf'8902'__4
v10))
                                      ((T__'8715''8902'__14 -> T__'8866''8902'__20) -> Any -> Any
forall a b. a -> b
coe
                                         T__'8715''8902'__14 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'96'_22
                                         (T__'8715''8902'__14 -> Any
forall a b. a -> b
coe T__'8715''8902'__14
MAlonzo.Code.Type.C_Z_16)))))
                             (T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
MAlonzo.Code.Type.BetaNormal.d_embNf_128
                                (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4) (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v9) (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v11))))
                       (T_EC_476 -> Any
forall a b. a -> b
coe T_EC_476
v7) (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v2))
             T__'8866'Nf'8902'__4
_ -> T__'8866'__168
forall a. a
MAlonzo.RTE.mazUnreachableError
      C_unwrap_'47'__534 T_Kind_476
v3 T__'8866'Nf'8902'__4
v4 T__'8866'Nf'8902'__4
v5 T_EC_476
v8
        -> (T_Kind_476
 -> T__'8866'Nf'8902'__4
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> T__'8866'__168)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> Any
-> T__'8866'__168
forall a b. a -> b
coe
             T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'__168
MAlonzo.Code.Algorithmic.C_unwrap_220 T_Kind_476
v3 T__'8866'Nf'8902'__4
v4 T__'8866'Nf'8902'__4
v5
             ((T__'8866'Nf'8902'__4
 -> T_EC_476 -> T__'8866'__168 -> T__'8866'__168)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T__'8866'Nf'8902'__4
-> T_EC_476 -> T__'8866'__168 -> T__'8866'__168
du__'91'_'93''7473'_574
                ((T_Kind_476
 -> T__'8866'Nf'8902'__4
 -> T__'8866'Nf'8902'__4
 -> T__'8866'Nf'8902'__4)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> Any
forall a b. a -> b
coe T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_μ_24 T_Kind_476
v3 T__'8866'Nf'8902'__4
v4 T__'8866'Nf'8902'__4
v5) (T_EC_476 -> Any
forall a b. a -> b
coe T_EC_476
v8)
                (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v2))
      C_constr_558 T_Bwd_6
v4 T__'8866'Nf'8902'__4
v5 [T__'8866'Nf'8902'__4]
v6 T_Fin_6
v8 [T__'8866'Nf'8902'__4]
v10 T__'8803'_'60''62''62'__684
v12 T_IBwd_396
v13 T_IIBwd_832
v14 T_IList_302
v15 T_EC_476
v16
        -> (T_Fin_6
 -> [T__'8866'Nf'8902'__4] -> T_IList_302 -> T__'8866'__168)
-> T_Fin_6 -> Any -> Any -> T__'8866'__168
forall a b. a -> b
coe
             T_Fin_6 -> [T__'8866'Nf'8902'__4] -> T_IList_302 -> T__'8866'__168
MAlonzo.Code.Algorithmic.C_constr_230 T_Fin_6
v8
             ((T_Bwd_6 -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                T_Bwd_6 -> [Any] -> [Any]
MAlonzo.Code.Utils.List.du__'60''62''62'__42 (T_Bwd_6 -> Any
forall a b. a -> b
coe T_Bwd_6
v4)
                ((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'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v5) ([T__'8866'Nf'8902'__4] -> Any
forall a b. a -> b
coe [T__'8866'Nf'8902'__4]
v6)))
             ((T_Bwd_6 -> T_IBwd_396 -> T_IList_302 -> T_IList_302)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_Bwd_6 -> T_IBwd_396 -> T_IList_302 -> T_IList_302
MAlonzo.Code.Utils.List.du__'60''62''62'I__418 (T_Bwd_6 -> Any
forall a b. a -> b
coe T_Bwd_6
v4) (T_IBwd_396 -> Any
forall a b. a -> b
coe T_IBwd_396
v13)
                ((Any -> T_IList_302 -> T_IList_302) -> Any -> T_IList_302 -> Any
forall a b. a -> b
coe
                   Any -> T_IList_302 -> T_IList_302
MAlonzo.Code.Utils.List.C__'8759'__314
                   ((T__'8866'Nf'8902'__4
 -> T_EC_476 -> T__'8866'__168 -> T__'8866'__168)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
-> T_EC_476 -> T__'8866'__168 -> T__'8866'__168
du__'91'_'93''7473'_574 (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v5) (T_EC_476 -> Any
forall a b. a -> b
coe T_EC_476
v16) (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v2)) T_IList_302
v15))
      C_case_568 Integer
v5 T_Vec_24
v6 T_Cases_162
v7 T_EC_476
v8
        -> (Integer
 -> T_Vec_24 -> T__'8866'__168 -> T_Cases_162 -> T__'8866'__168)
-> Integer -> T_Vec_24 -> Any -> T_Cases_162 -> T__'8866'__168
forall a b. a -> b
coe
             Integer
-> T_Vec_24 -> T__'8866'__168 -> T_Cases_162 -> T__'8866'__168
MAlonzo.Code.Algorithmic.C_case_242 Integer
v5 T_Vec_24
v6
             ((T__'8866'Nf'8902'__4
 -> T_EC_476 -> T__'8866'__168 -> T__'8866'__168)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T__'8866'Nf'8902'__4
-> T_EC_476 -> T__'8866'__168 -> T__'8866'__168
du__'91'_'93''7473'_574
                ((Integer -> T_Vec_24 -> T__'8866'Nf'8902'__4)
-> Integer -> T_Vec_24 -> Any
forall a b. a -> b
coe Integer -> T_Vec_24 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_SOP_28 Integer
v5 T_Vec_24
v6) (T_EC_476 -> Any
forall a b. a -> b
coe T_EC_476
v8)
                (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v2))
             T_Cases_162
v7
      T_EC_476
_ -> T__'8866'__168
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algorithmic.ReductionEC.applyCase
d_applyCase_640 ::
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  [MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  MAlonzo.Code.Utils.List.T_IList_302 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168
d_applyCase_640 :: T__'8866'Nf'8902'__4
-> [T__'8866'Nf'8902'__4]
-> T__'8866'__168
-> T_IList_302
-> T__'8866'__168
d_applyCase_640 ~T__'8866'Nf'8902'__4
v0 [T__'8866'Nf'8902'__4]
v1 T__'8866'__168
v2 T_IList_302
v3 = [T__'8866'Nf'8902'__4]
-> T__'8866'__168 -> T_IList_302 -> T__'8866'__168
du_applyCase_640 [T__'8866'Nf'8902'__4]
v1 T__'8866'__168
v2 T_IList_302
v3
du_applyCase_640 ::
  [MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  MAlonzo.Code.Utils.List.T_IList_302 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168
du_applyCase_640 :: [T__'8866'Nf'8902'__4]
-> T__'8866'__168 -> T_IList_302 -> T__'8866'__168
du_applyCase_640 [T__'8866'Nf'8902'__4]
v0 T__'8866'__168
v1 T_IList_302
v2
  = case T_IList_302 -> T_IList_302
forall a b. a -> b
coe T_IList_302
v2 of
      T_IList_302
MAlonzo.Code.Utils.List.C_'91''93'_308 -> T__'8866'__168 -> T__'8866'__168
forall a b. a -> b
coe T__'8866'__168
v1
      MAlonzo.Code.Utils.List.C__'8759'__314 Any
v5 T_IList_302
v6
        -> case [T__'8866'Nf'8902'__4] -> [Any]
forall a b. a -> b
coe [T__'8866'Nf'8902'__4]
v0 of
             (:) Any
v7 [Any]
v8
               -> ([T__'8866'Nf'8902'__4]
 -> T__'8866'__168 -> T_IList_302 -> T__'8866'__168)
-> Any -> Any -> Any -> T__'8866'__168
forall a b. a -> b
coe
                    [T__'8866'Nf'8902'__4]
-> T__'8866'__168 -> T_IList_302 -> T__'8866'__168
du_applyCase_640 ([Any] -> Any
forall a b. a -> b
coe [Any]
v8)
                    ((T__'8866'Nf'8902'__4
 -> T__'8866'__168 -> T__'8866'__168 -> T__'8866'__168)
-> Any -> T__'8866'__168 -> Any -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
-> T__'8866'__168 -> T__'8866'__168 -> T__'8866'__168
MAlonzo.Code.Algorithmic.C__'183'__186 Any
v7 T__'8866'__168
v1 Any
v5) (T_IList_302 -> Any
forall a b. a -> b
coe T_IList_302
v6)
             [Any]
_ -> T__'8866'__168
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_IList_302
_ -> T__'8866'__168
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algorithmic.ReductionEC._—→⋆_
d__'8212''8594''8902'__652 :: p -> p -> p -> ()
d__'8212''8594''8902'__652 p
a0 p
a1 p
a2 = ()
data T__'8212''8594''8902'__652
  = C_β'45'ƛ_662 T_Value_28 | C_β'45'Λ_678 |
    C_β'45'wrap_694 T_Value_28 |
    C_β'45'builtin_720 Integer MAlonzo.Code.Builtin.T_Builtin_2
                       MAlonzo.Code.Utils.T__'8724'_'8803'__120 Integer
                       MAlonzo.Code.Utils.T__'8724'_'8803'__120
                       MAlonzo.Code.Builtin.Signature.T_SigTy_260 T_BApp_74 T_Value_28 |
    C_β'45'case_746 MAlonzo.Code.Utils.List.T_Bwd_6
                    MAlonzo.Code.Utils.List.T_IBwd_396
                    MAlonzo.Code.Utils.List.T_IIBwd_832
-- Algorithmic.ReductionEC._—→_
d__'8212''8594'__750 :: p -> p -> p -> ()
d__'8212''8594'__750 p
a0 p
a1 p
a2 = ()
data T__'8212''8594'__750
  = C_ruleEC_766 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
                 MAlonzo.Code.Algorithmic.T__'8866'__168
                 MAlonzo.Code.Algorithmic.T__'8866'__168 T_EC_476
                 T__'8212''8594''8902'__652 |
    C_ruleErr_776 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
                  T_EC_476
-- Algorithmic.ReductionEC._—↠_
d__'8212''8608'__780 :: p -> p -> p -> ()
d__'8212''8608'__780 p
a0 p
a1 p
a2 = ()
data T__'8212''8608'__780
  = C_refl'8212''8608'_786 |
    C_trans'8212''8608'_796 MAlonzo.Code.Algorithmic.T__'8866'__168
                            T__'8212''8594'__750 T__'8212''8608'__780
-- Algorithmic.ReductionEC.V-I
d_V'45'I_818 ::
  MAlonzo.Code.Builtin.T_Builtin_2 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  Integer ->
  Integer ->
  MAlonzo.Code.Utils.T__'8724'_'8803'__120 ->
  Integer ->
  Integer ->
  MAlonzo.Code.Utils.T__'8724'_'8803'__120 ->
  MAlonzo.Code.Builtin.Signature.T_SigTy_260 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 -> T_BApp_74 -> T_Value_28
d_V'45'I_818 :: T_Builtin_2
-> T__'8866'Nf'8902'__4
-> Integer
-> Integer
-> T__'8724'_'8803'__120
-> Integer
-> Integer
-> T__'8724'_'8803'__120
-> T_SigTy_260
-> T__'8866'__168
-> T_BApp_74
-> T_Value_28
d_V'45'I_818 T_Builtin_2
v0 ~T__'8866'Nf'8902'__4
v1 Integer
v2 Integer
v3 T__'8724'_'8803'__120
v4 Integer
v5 Integer
v6 T__'8724'_'8803'__120
v7 T_SigTy_260
v8 ~T__'8866'__168
v9 T_BApp_74
v10
  = T_Builtin_2
-> Integer
-> Integer
-> T__'8724'_'8803'__120
-> Integer
-> Integer
-> T__'8724'_'8803'__120
-> T_SigTy_260
-> T_BApp_74
-> T_Value_28
du_V'45'I_818 T_Builtin_2
v0 Integer
v2 Integer
v3 T__'8724'_'8803'__120
v4 Integer
v5 Integer
v6 T__'8724'_'8803'__120
v7 T_SigTy_260
v8 T_BApp_74
v10
du_V'45'I_818 ::
  MAlonzo.Code.Builtin.T_Builtin_2 ->
  Integer ->
  Integer ->
  MAlonzo.Code.Utils.T__'8724'_'8803'__120 ->
  Integer ->
  Integer ->
  MAlonzo.Code.Utils.T__'8724'_'8803'__120 ->
  MAlonzo.Code.Builtin.Signature.T_SigTy_260 ->
  T_BApp_74 -> T_Value_28
du_V'45'I_818 :: T_Builtin_2
-> Integer
-> Integer
-> T__'8724'_'8803'__120
-> Integer
-> Integer
-> T__'8724'_'8803'__120
-> T_SigTy_260
-> T_BApp_74
-> T_Value_28
du_V'45'I_818 T_Builtin_2
v0 Integer
v1 Integer
v2 T__'8724'_'8803'__120
v3 Integer
v4 Integer
v5 T__'8724'_'8803'__120
v6 T_SigTy_260
v7 T_BApp_74
v8
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v2 of
      Integer
0 -> case T_SigTy_260 -> T_SigTy_260
forall a b. a -> b
coe T_SigTy_260
v7 of
             MAlonzo.Code.Builtin.Signature.C__B'8658'__296 Any
v17 Any
v18 T_SigTy_260
v19
               -> (T_Builtin_2
 -> Integer
 -> T__'8724'_'8803'__120
 -> Integer
 -> Integer
 -> T__'8724'_'8803'__120
 -> T_SigTy_260
 -> T_BApp_74
 -> T_Value_28)
-> T_Builtin_2
-> Integer
-> T__'8724'_'8803'__120
-> Integer
-> Integer
-> T__'8724'_'8803'__120
-> T_SigTy_260
-> T_BApp_74
-> T_Value_28
forall a b. a -> b
coe T_Builtin_2
-> Integer
-> T__'8724'_'8803'__120
-> Integer
-> Integer
-> T__'8724'_'8803'__120
-> T_SigTy_260
-> T_BApp_74
-> T_Value_28
C_V'45'I'8658'_184 T_Builtin_2
v0 Integer
v1 T__'8724'_'8803'__120
v3 Integer
v4 Integer
v5 T__'8724'_'8803'__120
v6 T_SigTy_260
v19 T_BApp_74
v8
             T_SigTy_260
_ -> T_Value_28
forall a. a
MAlonzo.RTE.mazUnreachableError
      Integer
_ -> let v9 :: Integer
v9 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> T_Value_28
forall a b. a -> b
coe
             (case T_SigTy_260 -> T_SigTy_260
forall a b. a -> b
coe T_SigTy_260
v7 of
                MAlonzo.Code.Builtin.Signature.C_sucΠ_320 T_Kind_476
v19 Any
v20 T_SigTy_260
v21
                  -> (T_Builtin_2
 -> Integer
 -> Integer
 -> T__'8724'_'8803'__120
 -> Integer
 -> Integer
 -> T__'8724'_'8803'__120
 -> T_SigTy_260
 -> T_BApp_74
 -> T_Value_28)
-> T_Builtin_2
-> Integer
-> Integer
-> T__'8724'_'8803'__120
-> Integer
-> Integer
-> T__'8724'_'8803'__120
-> T_SigTy_260
-> T_BApp_74
-> Any
forall a b. a -> b
coe T_Builtin_2
-> Integer
-> Integer
-> T__'8724'_'8803'__120
-> Integer
-> Integer
-> T__'8724'_'8803'__120
-> T_SigTy_260
-> T_BApp_74
-> T_Value_28
C_V'45'IΠ_208 T_Builtin_2
v0 Integer
v1 Integer
v9 T__'8724'_'8803'__120
v3 Integer
v4 Integer
v5 T__'8724'_'8803'__120
v6 T_SigTy_260
v21 T_BApp_74
v8
                T_SigTy_260
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Algorithmic.ReductionEC.ival
d_ival_838 :: MAlonzo.Code.Builtin.T_Builtin_2 -> T_Value_28
d_ival_838 :: T_Builtin_2 -> T_Value_28
d_ival_838 T_Builtin_2
v0
  = (T_Builtin_2
 -> Integer
 -> Integer
 -> T__'8724'_'8803'__120
 -> Integer
 -> Integer
 -> T__'8724'_'8803'__120
 -> T_SigTy_260
 -> T_BApp_74
 -> T_Value_28)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> T_Value_28
forall a b. a -> b
coe
      T_Builtin_2
-> Integer
-> Integer
-> T__'8724'_'8803'__120
-> Integer
-> Integer
-> T__'8724'_'8803'__120
-> T_SigTy_260
-> T_BApp_74
-> T_Value_28
du_V'45'I_818 (T_Builtin_2 -> Any
forall a b. a -> b
coe T_Builtin_2
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
      ((T_Sig_68 -> Integer) -> Any -> Any
forall a b. a -> b
coe
         T_Sig_68 -> Integer
MAlonzo.Code.Builtin.Signature.d_fv_92
         ((T_Builtin_2 -> T_Sig_68) -> Any -> Any
forall a b. a -> b
coe T_Builtin_2 -> T_Sig_68
MAlonzo.Code.Builtin.d_signature_278 (T_Builtin_2 -> Any
forall a b. a -> b
coe T_Builtin_2
v0)))
      (T__'8724'_'8803'__120 -> Any
forall a b. a -> b
coe T__'8724'_'8803'__120
MAlonzo.Code.Utils.C_start_124) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
      (((Any -> Any -> Any) -> Any -> [Any] -> Any)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any -> Any) -> Any -> [Any] -> Any
MAlonzo.Code.Data.List.Base.du_foldr_240
         (let v1 :: a -> Integer
v1 = \ a
v1 -> Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (a -> Integer
forall a b. a -> b
coe a
v1) in
          Any -> Any
forall a b. a -> b
coe ((Any -> Any -> Integer) -> Any
forall a b. a -> b
coe (\ Any
v2 -> Any -> Integer
forall {a}. a -> Integer
v1)))
         (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
         ((T_List'8314'_24 -> [Any]) -> Any -> Any
forall a b. a -> b
coe
            T_List'8314'_24 -> [Any]
MAlonzo.Code.Data.List.NonEmpty.Base.d_tail_34
            ((T_Sig_68 -> T_List'8314'_24) -> Any -> Any
forall a b. a -> b
coe
               T_Sig_68 -> T_List'8314'_24
MAlonzo.Code.Builtin.Signature.d_args_82
               ((T_Builtin_2 -> T_Sig_68) -> Any -> Any
forall a b. a -> b
coe T_Builtin_2 -> T_Sig_68
MAlonzo.Code.Builtin.d_signature_278 (T_Builtin_2 -> Any
forall a b. a -> b
coe T_Builtin_2
v0)))))
      (T__'8724'_'8803'__120 -> Any
forall a b. a -> b
coe T__'8724'_'8803'__120
MAlonzo.Code.Utils.C_start_124)
      (((T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
 -> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
 -> (T_Ctx'8902'_2 -> Any -> Any)
 -> (T_Ctx'8902'_2 -> Any -> Any -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
 -> T_Sig_68
 -> T_SigTy_260)
-> (Any -> Any -> Any -> Any)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> (Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
forall a b. a -> b
coe
         (T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> T_Sig_68
-> T_SigTy_260
MAlonzo.Code.Builtin.Signature.du_sig2SigTy_392
         (\ Any
v1 Any
v2 Any
v3 -> (T__'8866'Ne'8902'__6 -> T__'8866'Nf'8902'__4) -> Any -> Any
forall a b. a -> b
coe T__'8866'Ne'8902'__6 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_ne_20 Any
v3)
         ((Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
            (\ Any
v1 Any
v2 Any
v3 Any
v4 -> (T__'8715''8902'__14 -> T__'8866'Ne'8902'__6) -> Any -> Any
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8866'Ne'8902'__6
MAlonzo.Code.Type.BetaNormal.C_'96'_8 Any
v4))
         (\ Any
v1 Any
v2 Any
v3 Any
v4 Any
v5 ->
            (T_Kind_476
 -> T__'8866'Ne'8902'__6
 -> T__'8866'Nf'8902'__4
 -> T__'8866'Ne'8902'__6)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Kind_476
-> T__'8866'Ne'8902'__6
-> T__'8866'Nf'8902'__4
-> T__'8866'Ne'8902'__6
MAlonzo.Code.Type.BetaNormal.C__'183'__10 Any
v2 Any
v4 Any
v5)
         ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v1 Any
v2 -> (T_TyCon_6 -> T__'8866'Ne'8902'__6) -> Any
forall a b. a -> b
coe T_TyCon_6 -> T__'8866'Ne'8902'__6
MAlonzo.Code.Type.BetaNormal.C_'94'_12))
         (\ Any
v1 Any
v2 -> (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4) -> Any -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_con_22 Any
v2)
         (\ Any
v1 Any
v2 Any
v3 ->
            (T__'8866'Nf'8902'__4
 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4)
-> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C__'8658'__16 Any
v2 Any
v3)
         (\ Any
v1 Any
v2 Any
v3 -> (T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_Π_14 Any
v2 Any
v3)
         ((T_Builtin_2 -> T_Sig_68) -> Any -> Any
forall a b. a -> b
coe T_Builtin_2 -> T_Sig_68
MAlonzo.Code.Builtin.d_signature_278 (T_Builtin_2 -> Any
forall a b. a -> b
coe T_Builtin_2
v0)))
      (T_BApp_74 -> Any
forall a b. a -> b
coe T_BApp_74
C_base_78)