{-# 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 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.Builtin
import qualified MAlonzo.Code.Builtin.Constant.Type
import qualified MAlonzo.Code.Builtin.Signature
import qualified MAlonzo.Code.Data.Fin.Base
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.Vec.Base
import qualified MAlonzo.Code.Type
import qualified MAlonzo.Code.Type.BetaNormal
import qualified MAlonzo.Code.Utils
import qualified MAlonzo.Code.Utils.List

-- Algorithmic.Ctx
d_Ctx_2 :: p -> ()
d_Ctx_2 p
a0 = ()
data T_Ctx_2
  = C_'8709'_4 | C__'44''8902'__8 T_Ctx_2 |
    C__'44'__12 T_Ctx_2
                MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
-- Algorithmic._∋_
d__'8715'__16 :: p -> p -> p -> ()
d__'8715'__16 p
a0 p
a1 p
a2 = ()
data T__'8715'__16
  = C_Z_22 | C_S_30 T__'8715'__16 |
    C_T_38 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
           T__'8715'__16
-- Algorithmic.♯Kinded
d_'9839'Kinded_40 :: p -> ()
d_'9839'Kinded_40 p
a0 = ()
data T_'9839'Kinded_40
  = C_'9839'_42 | C_K'9839'_48 T_'9839'Kinded_40
-- Algorithmic.lemma♯Kinded
d_lemma'9839'Kinded_58 ::
  MAlonzo.Code.Utils.T_Kind_636 ->
  MAlonzo.Code.Utils.T_Kind_636 ->
  MAlonzo.Code.Utils.T_Kind_636 ->
  MAlonzo.Code.Utils.T_Kind_636 ->
  T_'9839'Kinded_40 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Ne'8902'__6 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_lemma'9839'Kinded_58 :: T_Kind_636
-> T_Kind_636
-> T_Kind_636
-> T_Kind_636
-> T_'9839'Kinded_40
-> T__'8866'Ne'8902'__6
-> T_Irrelevant_20
d_lemma'9839'Kinded_58 = T_Kind_636
-> T_Kind_636
-> T_Kind_636
-> T_Kind_636
-> T_'9839'Kinded_40
-> T__'8866'Ne'8902'__6
-> T_Irrelevant_20
forall a. a
erased
-- Algorithmic.ty2sty
d_ty2sty_64 ::
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4
d_ty2sty_64 :: T__'8866'Nf'8902'__4 -> T__'8866''9839'_4
d_ty2sty_64 T__'8866'Nf'8902'__4
v0
  = 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_ne_20 T__'8866'Ne'8902'__6
v3
        -> case T__'8866'Ne'8902'__6 -> T__'8866'Ne'8902'__6
forall a b. a -> b
coe T__'8866'Ne'8902'__6
v3 of
             MAlonzo.Code.Type.BetaNormal.C__'183'__10 T_Kind_636
v5 T__'8866'Ne'8902'__6
v7 T__'8866'Nf'8902'__4
v8
               -> case T__'8866'Ne'8902'__6 -> T__'8866'Ne'8902'__6
forall a b. a -> b
coe T__'8866'Ne'8902'__6
v7 of
                    MAlonzo.Code.Type.BetaNormal.C__'183'__10 T_Kind_636
v10 T__'8866'Ne'8902'__6
v12 T__'8866'Nf'8902'__4
v13
                      -> case T__'8866'Ne'8902'__6 -> T__'8866'Ne'8902'__6
forall a b. a -> b
coe T__'8866'Ne'8902'__6
v12 of
                           MAlonzo.Code.Type.BetaNormal.C_'94'_12 T_TyCon_6
v16
                             -> (Any -> Any -> Any) -> Any -> Any -> T__'8866''9839'_4
forall a b. a -> b
coe
                                  Any -> Any -> Any
forall a b. a -> b -> b
seq (T_TyCon_6 -> Any
forall a b. a -> b
coe T_TyCon_6
v16)
                                  ((T__'8866''9839'_4 -> T__'8866''9839'_4 -> T__'8866''9839'_4)
-> T__'8866''9839'_4 -> T__'8866''9839'_4 -> Any
forall a b. a -> b
coe
                                     T__'8866''9839'_4 -> T__'8866''9839'_4 -> T__'8866''9839'_4
MAlonzo.Code.Builtin.Signature.C_pair_20
                                     (T__'8866'Nf'8902'__4 -> T__'8866''9839'_4
d_ty2sty_64 (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v13)) (T__'8866'Nf'8902'__4 -> T__'8866''9839'_4
d_ty2sty_64 (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v8)))
                           T__'8866'Ne'8902'__6
_ -> T__'8866''9839'_4
forall a. a
MAlonzo.RTE.mazUnreachableError
                    MAlonzo.Code.Type.BetaNormal.C_'94'_12 T_TyCon_6
v11
                      -> (Any -> Any -> Any) -> Any -> Any -> T__'8866''9839'_4
forall a b. a -> b
coe
                           Any -> Any -> Any
forall a b. a -> b -> b
seq (T_TyCon_6 -> Any
forall a b. a -> b
coe T_TyCon_6
v11)
                           ((T__'8866''9839'_4 -> T__'8866''9839'_4)
-> T__'8866''9839'_4 -> Any
forall a b. a -> b
coe
                              T__'8866''9839'_4 -> T__'8866''9839'_4
MAlonzo.Code.Builtin.Signature.C_list_16 (T__'8866'Nf'8902'__4 -> T__'8866''9839'_4
d_ty2sty_64 (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v8)))
                    T__'8866'Ne'8902'__6
_ -> T__'8866''9839'_4
forall a. a
MAlonzo.RTE.mazUnreachableError
             MAlonzo.Code.Type.BetaNormal.C_'94'_12 T_TyCon_6
v6
               -> case T_TyCon_6 -> T_TyCon_6
forall a b. a -> b
coe T_TyCon_6
v6 of
                    MAlonzo.Code.Builtin.Constant.Type.C_atomic_8 T_AtomicTyCon_6
v7
                      -> (T_AtomicTyCon_6 -> T__'8866''9839'_4)
-> T_AtomicTyCon_6 -> T__'8866''9839'_4
forall a b. a -> b
coe T_AtomicTyCon_6 -> T__'8866''9839'_4
MAlonzo.Code.Builtin.Signature.C_atomic_12 T_AtomicTyCon_6
v7
                    T_TyCon_6
_ -> T__'8866''9839'_4
forall a. a
MAlonzo.RTE.mazUnreachableError
             T__'8866'Ne'8902'__6
_ -> T__'8866''9839'_4
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8866'Nf'8902'__4
_ -> T__'8866''9839'_4
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algorithmic.sty2ty
d_sty2ty_82 ::
  MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
d_sty2ty_82 :: T__'8866''9839'_4 -> T__'8866'Nf'8902'__4
d_sty2ty_82 T__'8866''9839'_4
v0
  = (T__'8866'Ne'8902'__6 -> T__'8866'Nf'8902'__4)
-> Any -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
      T__'8866'Ne'8902'__6 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_ne_20
      (((T_Ctx'8902'_2 -> T_Kind_636 -> Any -> Any)
 -> (Integer -> Integer -> T_Kind_636 -> T__'8715''8902'__14 -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_636 -> T_Kind_636 -> Any -> Any -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_636 -> T_TyCon_6 -> Any)
 -> Integer
 -> Integer
 -> T__'8866''9839'_4
 -> 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_636 -> Any -> Any)
-> (Integer -> Integer -> T_Kind_636 -> T__'8715''8902'__14 -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_636 -> T_Kind_636 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_636 -> T_TyCon_6 -> Any)
-> Integer
-> Integer
-> T__'8866''9839'_4
-> Any
MAlonzo.Code.Builtin.Signature.du_'8866''9839'2TyNe'9839'_182
         (\ 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_636
 -> 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_636
-> 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))
         (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (T__'8866''9839'_4 -> Any
forall a b. a -> b
coe T__'8866''9839'_4
v0))
-- Algorithmic.ty≅sty₁
d_ty'8773'sty'8321'_88 ::
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_ty'8773'sty'8321'_88 :: T__'8866'Nf'8902'__4 -> T__'8801'__12
d_ty'8773'sty'8321'_88 = T__'8866'Nf'8902'__4 -> T__'8801'__12
forall a. a
erased
-- Algorithmic.ty≅sty₂
d_ty'8773'sty'8322'_112 ::
  MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_ty'8773'sty'8322'_112 :: T__'8866''9839'_4 -> T__'8801'__12
d_ty'8773'sty'8322'_112 = T__'8866''9839'_4 -> T__'8801'__12
forall a. a
erased
-- Algorithmic.⟦_⟧
d_'10214'_'10215'_124 ::
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 -> ()
d_'10214'_'10215'_124 :: T__'8866'Nf'8902'__4 -> ()
d_'10214'_'10215'_124 = T__'8866'Nf'8902'__4 -> ()
forall a. a
erased
-- Algorithmic.mkCaseType
d_mkCaseType_146 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  [MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
d_mkCaseType_146 :: T_Ctx'8902'_2
-> T__'8866'Nf'8902'__4
-> [T__'8866'Nf'8902'__4]
-> T__'8866'Nf'8902'__4
d_mkCaseType_146 ~T_Ctx'8902'_2
v0 T__'8866'Nf'8902'__4
v1 = T__'8866'Nf'8902'__4
-> [T__'8866'Nf'8902'__4] -> T__'8866'Nf'8902'__4
du_mkCaseType_146 T__'8866'Nf'8902'__4
v1
du_mkCaseType_146 ::
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  [MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
du_mkCaseType_146 :: T__'8866'Nf'8902'__4
-> [T__'8866'Nf'8902'__4] -> T__'8866'Nf'8902'__4
du_mkCaseType_146 T__'8866'Nf'8902'__4
v0
  = ((Any -> Any -> Any) -> Any -> [Any] -> Any)
-> Any -> Any -> [T__'8866'Nf'8902'__4] -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
      (Any -> Any -> Any) -> Any -> [Any] -> Any
MAlonzo.Code.Data.List.Base.du_foldr_216
      ((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 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v0)
-- Algorithmic.ConstrArgs
d_ConstrArgs_152 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  T_Ctx_2 ->
  [MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] -> ()
d_ConstrArgs_152 :: T_Ctx'8902'_2 -> T_Ctx_2 -> [T__'8866'Nf'8902'__4] -> ()
d_ConstrArgs_152 = T_Ctx'8902'_2 -> T_Ctx_2 -> [T__'8866'Nf'8902'__4] -> ()
forall a. a
erased
-- Algorithmic.Cases
d_Cases_162 :: p -> p -> p -> p -> p -> ()
d_Cases_162 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
data T_Cases_162
  = C_'91''93'_268 | C__'8759'__280 T__'8866'__168 T_Cases_162
-- Algorithmic._⊢_
d__'8866'__168 :: p -> p -> p -> ()
d__'8866'__168 p
a0 p
a1 p
a2 = ()
data T__'8866'__168
  = C_'96'_174 T__'8715'__16 | C_ƛ_180 T__'8866'__168 |
    C__'183'__186 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
                  T__'8866'__168 T__'8866'__168 |
    C_Λ_192 T__'8866'__168 |
    C__'183''8902'_'47'__202 MAlonzo.Code.Utils.T_Kind_636
                             MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 T__'8866'__168
                             MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 |
    C_wrap_210 T__'8866'__168 |
    C_unwrap_220 MAlonzo.Code.Utils.T_Kind_636
                 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
                 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 T__'8866'__168 |
    C_constr_230 MAlonzo.Code.Data.Fin.Base.T_Fin_10
                 [MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4]
                 MAlonzo.Code.Utils.List.T_IList_302 |
    C_case_242 Integer MAlonzo.Code.Data.Vec.Base.T_Vec_28
               T__'8866'__168 T_Cases_162 |
    C_con_248 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
              AgdaAny |
    C_builtin_'47'__254 MAlonzo.Code.Builtin.T_Builtin_2 | C_error_258
-- Algorithmic.conv∋
d_conv'8715'_290 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  T_Ctx_2 ->
  T_Ctx_2 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__'8715'__16 -> T__'8715'__16
d_conv'8715'_290 :: T_Ctx'8902'_2
-> T_Ctx_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
-> T__'8801'__12
-> T__'8715'__16
-> T__'8715'__16
d_conv'8715'_290 ~T_Ctx'8902'_2
v0 ~T_Ctx_2
v1 ~T_Ctx_2
v2 ~T__'8866'Nf'8902'__4
v3 ~T__'8866'Nf'8902'__4
v4 ~T__'8801'__12
v5 ~T__'8801'__12
v6 T__'8715'__16
v7
  = T__'8715'__16 -> T__'8715'__16
du_conv'8715'_290 T__'8715'__16
v7
du_conv'8715'_290 :: T__'8715'__16 -> T__'8715'__16
du_conv'8715'_290 :: T__'8715'__16 -> T__'8715'__16
du_conv'8715'_290 T__'8715'__16
v0 = T__'8715'__16 -> T__'8715'__16
forall a b. a -> b
coe T__'8715'__16
v0
-- Algorithmic.conv⊢
d_conv'8866'_302 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  T_Ctx_2 ->
  T_Ctx_2 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__'8866'__168 -> T__'8866'__168
d_conv'8866'_302 :: T_Ctx'8902'_2
-> T_Ctx_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
-> T__'8801'__12
-> T__'8866'__168
-> T__'8866'__168
d_conv'8866'_302 ~T_Ctx'8902'_2
v0 ~T_Ctx_2
v1 ~T_Ctx_2
v2 ~T__'8866'Nf'8902'__4
v3 ~T__'8866'Nf'8902'__4
v4 ~T__'8801'__12
v5 ~T__'8801'__12
v6 T__'8866'__168
v7
  = T__'8866'__168 -> T__'8866'__168
du_conv'8866'_302 T__'8866'__168
v7
du_conv'8866'_302 :: T__'8866'__168 -> T__'8866'__168
du_conv'8866'_302 :: T__'8866'__168 -> T__'8866'__168
du_conv'8866'_302 T__'8866'__168
v0 = T__'8866'__168 -> T__'8866'__168
forall a b. a -> b
coe T__'8866'__168
v0
-- Algorithmic.lookupCase
d_lookupCase_318 ::
  Integer ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  T_Ctx_2 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
  T_Cases_162 -> T__'8866'__168
d_lookupCase_318 :: Integer
-> T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T_Vec_28
-> T_Fin_10
-> T_Cases_162
-> T__'8866'__168
d_lookupCase_318 ~Integer
v0 ~T_Ctx'8902'_2
v1 ~T_Ctx_2
v2 ~T__'8866'Nf'8902'__4
v3 T_Vec_28
v4 T_Fin_10
v5 T_Cases_162
v6
  = T_Vec_28 -> T_Fin_10 -> T_Cases_162 -> T__'8866'__168
du_lookupCase_318 T_Vec_28
v4 T_Fin_10
v5 T_Cases_162
v6
du_lookupCase_318 ::
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
  T_Cases_162 -> T__'8866'__168
du_lookupCase_318 :: T_Vec_28 -> T_Fin_10 -> T_Cases_162 -> T__'8866'__168
du_lookupCase_318 T_Vec_28
v0 T_Fin_10
v1 T_Cases_162
v2
  = case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v1 of
      T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12
        -> case T_Cases_162 -> T_Cases_162
forall a b. a -> b
coe T_Cases_162
v2 of
             C__'8759'__280 T__'8866'__168
v7 T_Cases_162
v8 -> T__'8866'__168 -> T__'8866'__168
forall a b. a -> b
coe T__'8866'__168
v7
             T_Cases_162
_ -> T__'8866'__168
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_10
v4
        -> case T_Cases_162 -> T_Cases_162
forall a b. a -> b
coe T_Cases_162
v2 of
             C__'8759'__280 T__'8866'__168
v8 T_Cases_162
v9
               -> case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v0 of
                    MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v11 T_Vec_28
v12
                      -> (T_Vec_28 -> T_Fin_10 -> T_Cases_162 -> T__'8866'__168)
-> Any -> Any -> Any -> T__'8866'__168
forall a b. a -> b
coe T_Vec_28 -> T_Fin_10 -> T_Cases_162 -> T__'8866'__168
du_lookupCase_318 (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v12) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v4) (T_Cases_162 -> Any
forall a b. a -> b
coe T_Cases_162
v9)
                    T_Vec_28
_ -> T__'8866'__168
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_Cases_162
_ -> T__'8866'__168
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Fin_10
_ -> T__'8866'__168
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algorithmic.bwdMkCaseType
d_bwdMkCaseType_334 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  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
d_bwdMkCaseType_334 :: T_Ctx'8902'_2
-> T_Bwd_6 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
d_bwdMkCaseType_334 ~T_Ctx'8902'_2
v0 T_Bwd_6
v1 T__'8866'Nf'8902'__4
v2 = T_Bwd_6 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
du_bwdMkCaseType_334 T_Bwd_6
v1 T__'8866'Nf'8902'__4
v2
du_bwdMkCaseType_334 ::
  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
du_bwdMkCaseType_334 :: T_Bwd_6 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
du_bwdMkCaseType_334 T_Bwd_6
v0 T__'8866'Nf'8902'__4
v1
  = ((Any -> Any -> Any) -> Any -> T_Bwd_6 -> Any)
-> Any -> Any -> Any -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
      (Any -> Any -> Any) -> Any -> T_Bwd_6 -> Any
MAlonzo.Code.Utils.List.du_bwd'45'foldr_26
      ((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 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v1) (T_Bwd_6 -> Any
forall a b. a -> b
coe T_Bwd_6
v0)
-- Algorithmic.lemma-bwdfwdfunction'
d_lemma'45'bwdfwdfunction''_346 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  [MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lemma'45'bwdfwdfunction''_346 :: T_Ctx'8902'_2
-> T__'8866'Nf'8902'__4 -> [T__'8866'Nf'8902'__4] -> T__'8801'__12
d_lemma'45'bwdfwdfunction''_346 = T_Ctx'8902'_2
-> T__'8866'Nf'8902'__4 -> [T__'8866'Nf'8902'__4] -> T__'8801'__12
forall a. a
erased
-- Algorithmic.constr-cong
d_constr'45'cong_372 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  T_Ctx_2 ->
  Integer ->
  MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  [MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Utils.List.T_IList_302 ->
  MAlonzo.Code.Utils.List.T_IList_302 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_constr'45'cong_372 :: T_Ctx'8902'_2
-> T_Ctx_2
-> Integer
-> T_Fin_10
-> T_Vec_28
-> [T__'8866'Nf'8902'__4]
-> T__'8801'__12
-> T_IList_302
-> T_IList_302
-> T__'8801'__12
-> T__'8801'__12
d_constr'45'cong_372 = T_Ctx'8902'_2
-> T_Ctx_2
-> Integer
-> T_Fin_10
-> T_Vec_28
-> [T__'8866'Nf'8902'__4]
-> T__'8801'__12
-> T_IList_302
-> T_IList_302
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Algorithmic.constr-cong'
d_constr'45'cong''_400 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  T_Ctx_2 ->
  Integer ->
  MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  [MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] ->
  [MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Utils.List.T_IList_302 ->
  MAlonzo.Code.Utils.List.T_IList_302 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_constr'45'cong''_400 :: T_Ctx'8902'_2
-> T_Ctx_2
-> Integer
-> T_Fin_10
-> T_Vec_28
-> [T__'8866'Nf'8902'__4]
-> [T__'8866'Nf'8902'__4]
-> T__'8801'__12
-> T__'8801'__12
-> T_IList_302
-> T_IList_302
-> T__'8801'__12
-> T__'8801'__12
d_constr'45'cong''_400 = T_Ctx'8902'_2
-> T_Ctx_2
-> Integer
-> T_Fin_10
-> T_Vec_28
-> [T__'8866'Nf'8902'__4]
-> [T__'8866'Nf'8902'__4]
-> T__'8801'__12
-> T__'8801'__12
-> T_IList_302
-> T_IList_302
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased