{-# 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.AtomicType
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_782 ->
  MAlonzo.Code.Utils.T_Kind_782 ->
  MAlonzo.Code.Utils.T_Kind_782 ->
  MAlonzo.Code.Utils.T_Kind_782 ->
  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_782
-> T_Kind_782
-> T_Kind_782
-> T_Kind_782
-> T_'9839'Kinded_40
-> T__'8866'Ne'8902'__6
-> T_Irrelevant_20
d_lemma'9839'Kinded_58 = T_Kind_782
-> T_Kind_782
-> T_Kind_782
-> T_Kind_782
-> 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_782
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_782
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_24
                                     (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
                      -> case T_TyCon_6 -> T_TyCon_6
forall a b. a -> b
coe T_TyCon_6
v11 of
                           T_TyCon_6
MAlonzo.Code.Builtin.Constant.Type.C_list_10
                             -> (T__'8866''9839'_4 -> T__'8866''9839'_4)
-> T__'8866''9839'_4 -> T__'8866''9839'_4
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_TyCon_6
MAlonzo.Code.Builtin.Constant.Type.C_array_12
                             -> (T__'8866''9839'_4 -> T__'8866''9839'_4)
-> T__'8866''9839'_4 -> T__'8866''9839'_4
forall a b. a -> b
coe
                                  T__'8866''9839'_4 -> T__'8866''9839'_4
MAlonzo.Code.Builtin.Signature.C_array_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
v8))
                           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
             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_84 ::
  MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
d_sty2ty_84 :: T__'8866''9839'_4 -> T__'8866'Nf'8902'__4
d_sty2ty_84 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_782 -> Any -> Any)
 -> (Integer -> Integer -> T_Kind_782 -> T__'8715''8902'__14 -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_782 -> T_Kind_782 -> Any -> Any -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_782 -> 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_782 -> Any -> Any)
-> (Integer -> Integer -> T_Kind_782 -> T__'8715''8902'__14 -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_782 -> T_Kind_782 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_782 -> T_TyCon_6 -> Any)
-> Integer
-> Integer
-> T__'8866''9839'_4
-> Any
MAlonzo.Code.Builtin.Signature.du_'8866''9839'2TyNe'9839'_188
         (\ 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_782
 -> 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_782
-> 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'_90 ::
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_ty'8773'sty'8321'_90 :: T__'8866'Nf'8902'__4 -> T__'8801'__12
d_ty'8773'sty'8321'_90 = T__'8866'Nf'8902'__4 -> T__'8801'__12
forall a. a
erased
-- Algorithmic.ty≅sty₂
d_ty'8773'sty'8322'_118 ::
  MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_ty'8773'sty'8322'_118 :: T__'8866''9839'_4 -> T__'8801'__12
d_ty'8773'sty'8322'_118 = T__'8866''9839'_4 -> T__'8801'__12
forall a. a
erased
-- Algorithmic.con-atomic
d_con'45'atomic_132 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Builtin.Constant.AtomicType.T_AtomicTyCon_6 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
d_con'45'atomic_132 :: T_Ctx'8902'_2 -> T_AtomicTyCon_6 -> T__'8866'Nf'8902'__4
d_con'45'atomic_132 ~T_Ctx'8902'_2
v0 T_AtomicTyCon_6
v1 = T_AtomicTyCon_6 -> T__'8866'Nf'8902'__4
du_con'45'atomic_132 T_AtomicTyCon_6
v1
du_con'45'atomic_132 ::
  MAlonzo.Code.Builtin.Constant.AtomicType.T_AtomicTyCon_6 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
du_con'45'atomic_132 :: T_AtomicTyCon_6 -> T__'8866'Nf'8902'__4
du_con'45'atomic_132 T_AtomicTyCon_6
v0
  = (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4)
-> Any -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
      T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_con_22
      ((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
         ((T_TyCon_6 -> T__'8866'Ne'8902'__6) -> Any -> Any
forall a b. a -> b
coe
            T_TyCon_6 -> T__'8866'Ne'8902'__6
MAlonzo.Code.Type.BetaNormal.C_'94'_12
            ((T_AtomicTyCon_6 -> T_TyCon_6) -> Any -> Any
forall a b. a -> b
coe T_AtomicTyCon_6 -> T_TyCon_6
MAlonzo.Code.Builtin.Constant.Type.C_atomic_8 (T_AtomicTyCon_6 -> Any
forall a b. a -> b
coe T_AtomicTyCon_6
v0))))
-- Algorithmic.⟦_⟧
d_'10214'_'10215'_138 ::
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 -> ()
d_'10214'_'10215'_138 :: T__'8866'Nf'8902'__4 -> ()
d_'10214'_'10215'_138 = T__'8866'Nf'8902'__4 -> ()
forall a. a
erased
-- Algorithmic.mkCaseType
d_mkCaseType_162 ::
  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_162 :: T_Ctx'8902'_2
-> T__'8866'Nf'8902'__4
-> [T__'8866'Nf'8902'__4]
-> T__'8866'Nf'8902'__4
d_mkCaseType_162 ~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_162 T__'8866'Nf'8902'__4
v1
du_mkCaseType_162 ::
  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_162 :: T__'8866'Nf'8902'__4
-> [T__'8866'Nf'8902'__4] -> T__'8866'Nf'8902'__4
du_mkCaseType_162 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_168 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  T_Ctx_2 ->
  [MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] -> ()
d_ConstrArgs_168 :: T_Ctx'8902'_2 -> T_Ctx_2 -> [T__'8866'Nf'8902'__4] -> ()
d_ConstrArgs_168 = T_Ctx'8902'_2 -> T_Ctx_2 -> [T__'8866'Nf'8902'__4] -> ()
forall a. a
erased
-- Algorithmic.Cases
d_Cases_178 :: p -> p -> p -> p -> p -> ()
d_Cases_178 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
data T_Cases_178
  = C_'91''93'_284 | C__'8759'__296 T__'8866'__184 T_Cases_178
-- Algorithmic._⊢_
d__'8866'__184 :: p -> p -> p -> ()
d__'8866'__184 p
a0 p
a1 p
a2 = ()
data T__'8866'__184
  = C_'96'_190 T__'8715'__16 | C_ƛ_196 T__'8866'__184 |
    C__'183'__202 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
                  T__'8866'__184 T__'8866'__184 |
    C_Λ_208 T__'8866'__184 |
    C__'183''8902'_'47'__218 MAlonzo.Code.Utils.T_Kind_782
                             MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 T__'8866'__184
                             MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 |
    C_wrap_226 T__'8866'__184 |
    C_unwrap_236 MAlonzo.Code.Utils.T_Kind_782
                 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
                 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 T__'8866'__184 |
    C_constr_246 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_258 Integer MAlonzo.Code.Data.Vec.Base.T_Vec_28
               T__'8866'__184 T_Cases_178 |
    C_con_264 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
              AgdaAny |
    C_builtin_'47'__270 MAlonzo.Code.Builtin.T_Builtin_2 | C_error_274
-- Algorithmic.conv∋
d_conv'8715'_306 ::
  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'_306 :: 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'_306 ~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'_306 T__'8715'__16
v7
du_conv'8715'_306 :: T__'8715'__16 -> T__'8715'__16
du_conv'8715'_306 :: T__'8715'__16 -> T__'8715'__16
du_conv'8715'_306 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'_318 ::
  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'__184 -> T__'8866'__184
d_conv'8866'_318 :: 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'__184
-> T__'8866'__184
d_conv'8866'_318 ~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'__184
v7
  = T__'8866'__184 -> T__'8866'__184
du_conv'8866'_318 T__'8866'__184
v7
du_conv'8866'_318 :: T__'8866'__184 -> T__'8866'__184
du_conv'8866'_318 :: T__'8866'__184 -> T__'8866'__184
du_conv'8866'_318 T__'8866'__184
v0 = T__'8866'__184 -> T__'8866'__184
forall a b. a -> b
coe T__'8866'__184
v0
-- Algorithmic.lookupCase
d_lookupCase_334 ::
  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_178 -> T__'8866'__184
d_lookupCase_334 :: Integer
-> T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T_Vec_28
-> T_Fin_10
-> T_Cases_178
-> T__'8866'__184
d_lookupCase_334 ~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_178
v6
  = T_Vec_28 -> T_Fin_10 -> T_Cases_178 -> T__'8866'__184
du_lookupCase_334 T_Vec_28
v4 T_Fin_10
v5 T_Cases_178
v6
du_lookupCase_334 ::
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
  T_Cases_178 -> T__'8866'__184
du_lookupCase_334 :: T_Vec_28 -> T_Fin_10 -> T_Cases_178 -> T__'8866'__184
du_lookupCase_334 T_Vec_28
v0 T_Fin_10
v1 T_Cases_178
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_178 -> T_Cases_178
forall a b. a -> b
coe T_Cases_178
v2 of
             C__'8759'__296 T__'8866'__184
v7 T_Cases_178
v8 -> T__'8866'__184 -> T__'8866'__184
forall a b. a -> b
coe T__'8866'__184
v7
             T_Cases_178
_ -> T__'8866'__184
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_10
v4
        -> case T_Cases_178 -> T_Cases_178
forall a b. a -> b
coe T_Cases_178
v2 of
             C__'8759'__296 T__'8866'__184
v8 T_Cases_178
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_178 -> T__'8866'__184)
-> Any -> Any -> Any -> T__'8866'__184
forall a b. a -> b
coe T_Vec_28 -> T_Fin_10 -> T_Cases_178 -> T__'8866'__184
du_lookupCase_334 (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_178 -> Any
forall a b. a -> b
coe T_Cases_178
v9)
                    T_Vec_28
_ -> T__'8866'__184
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_Cases_178
_ -> T__'8866'__184
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Fin_10
_ -> T__'8866'__184
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algorithmic.bwdMkCaseType
d_bwdMkCaseType_350 ::
  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_350 :: T_Ctx'8902'_2
-> T_Bwd_6 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
d_bwdMkCaseType_350 ~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_350 T_Bwd_6
v1 T__'8866'Nf'8902'__4
v2
du_bwdMkCaseType_350 ::
  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_350 :: T_Bwd_6 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
du_bwdMkCaseType_350 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''_362 ::
  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''_362 :: T_Ctx'8902'_2
-> T__'8866'Nf'8902'__4 -> [T__'8866'Nf'8902'__4] -> T__'8801'__12
d_lemma'45'bwdfwdfunction''_362 = 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_388 ::
  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_388 :: 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_388 = 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''_416 ::
  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''_416 :: 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''_416 = 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