{-# 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_652 ->
  MAlonzo.Code.Utils.T_Kind_652 ->
  MAlonzo.Code.Utils.T_Kind_652 ->
  MAlonzo.Code.Utils.T_Kind_652 ->
  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_652
-> T_Kind_652
-> T_Kind_652
-> T_Kind_652
-> T_'9839'Kinded_40
-> T__'8866'Ne'8902'__6
-> T_Irrelevant_20
d_lemma'9839'Kinded_58 = T_Kind_652
-> T_Kind_652
-> T_Kind_652
-> T_Kind_652
-> 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_652
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_652
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_652 -> Any -> Any)
 -> (Integer -> Integer -> T_Kind_652 -> T__'8715''8902'__14 -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_652 -> T_Kind_652 -> Any -> Any -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_652 -> 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_652 -> Any -> Any)
-> (Integer -> Integer -> T_Kind_652 -> T__'8715''8902'__14 -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_652 -> T_Kind_652 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_652 -> T_TyCon_6 -> Any)
-> Integer
-> Integer
-> T__'8866''9839'_4
-> Any
MAlonzo.Code.Builtin.Signature.du_'8866''9839'2TyNe'9839'_186
         (\ 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_652
 -> 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_652
-> 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.⟦_⟧
d_'10214'_'10215'_132 ::
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 -> ()
d_'10214'_'10215'_132 :: T__'8866'Nf'8902'__4 -> ()
d_'10214'_'10215'_132 = T__'8866'Nf'8902'__4 -> ()
forall a. a
erased
-- Algorithmic.mkCaseType
d_mkCaseType_156 ::
  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_156 :: T_Ctx'8902'_2
-> T__'8866'Nf'8902'__4
-> [T__'8866'Nf'8902'__4]
-> T__'8866'Nf'8902'__4
d_mkCaseType_156 ~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_156 T__'8866'Nf'8902'__4
v1
du_mkCaseType_156 ::
  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_156 :: T__'8866'Nf'8902'__4
-> [T__'8866'Nf'8902'__4] -> T__'8866'Nf'8902'__4
du_mkCaseType_156 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_162 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  T_Ctx_2 ->
  [MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] -> ()
d_ConstrArgs_162 :: T_Ctx'8902'_2 -> T_Ctx_2 -> [T__'8866'Nf'8902'__4] -> ()
d_ConstrArgs_162 = T_Ctx'8902'_2 -> T_Ctx_2 -> [T__'8866'Nf'8902'__4] -> ()
forall a. a
erased
-- Algorithmic.Cases
d_Cases_172 :: p -> p -> p -> p -> p -> ()
d_Cases_172 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
data T_Cases_172
  = C_'91''93'_278 | C__'8759'__290 T__'8866'__178 T_Cases_172
-- Algorithmic._⊢_
d__'8866'__178 :: p -> p -> p -> ()
d__'8866'__178 p
a0 p
a1 p
a2 = ()
data T__'8866'__178
  = C_'96'_184 T__'8715'__16 | C_ƛ_190 T__'8866'__178 |
    C__'183'__196 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
                  T__'8866'__178 T__'8866'__178 |
    C_Λ_202 T__'8866'__178 |
    C__'183''8902'_'47'__212 MAlonzo.Code.Utils.T_Kind_652
                             MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 T__'8866'__178
                             MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 |
    C_wrap_220 T__'8866'__178 |
    C_unwrap_230 MAlonzo.Code.Utils.T_Kind_652
                 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
                 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 T__'8866'__178 |
    C_constr_240 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_252 Integer MAlonzo.Code.Data.Vec.Base.T_Vec_28
               T__'8866'__178 T_Cases_172 |
    C_con_258 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
              AgdaAny |
    C_builtin_'47'__264 MAlonzo.Code.Builtin.T_Builtin_2 | C_error_268
-- Algorithmic.conv∋
d_conv'8715'_300 ::
  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'_300 :: 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'_300 ~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'_300 T__'8715'__16
v7
du_conv'8715'_300 :: T__'8715'__16 -> T__'8715'__16
du_conv'8715'_300 :: T__'8715'__16 -> T__'8715'__16
du_conv'8715'_300 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'_312 ::
  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'__178 -> T__'8866'__178
d_conv'8866'_312 :: 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'__178
-> T__'8866'__178
d_conv'8866'_312 ~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'__178
v7
  = T__'8866'__178 -> T__'8866'__178
du_conv'8866'_312 T__'8866'__178
v7
du_conv'8866'_312 :: T__'8866'__178 -> T__'8866'__178
du_conv'8866'_312 :: T__'8866'__178 -> T__'8866'__178
du_conv'8866'_312 T__'8866'__178
v0 = T__'8866'__178 -> T__'8866'__178
forall a b. a -> b
coe T__'8866'__178
v0
-- Algorithmic.lookupCase
d_lookupCase_328 ::
  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_172 -> T__'8866'__178
d_lookupCase_328 :: Integer
-> T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T_Vec_28
-> T_Fin_10
-> T_Cases_172
-> T__'8866'__178
d_lookupCase_328 ~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_172
v6
  = T_Vec_28 -> T_Fin_10 -> T_Cases_172 -> T__'8866'__178
du_lookupCase_328 T_Vec_28
v4 T_Fin_10
v5 T_Cases_172
v6
du_lookupCase_328 ::
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
  T_Cases_172 -> T__'8866'__178
du_lookupCase_328 :: T_Vec_28 -> T_Fin_10 -> T_Cases_172 -> T__'8866'__178
du_lookupCase_328 T_Vec_28
v0 T_Fin_10
v1 T_Cases_172
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_172 -> T_Cases_172
forall a b. a -> b
coe T_Cases_172
v2 of
             C__'8759'__290 T__'8866'__178
v7 T_Cases_172
v8 -> T__'8866'__178 -> T__'8866'__178
forall a b. a -> b
coe T__'8866'__178
v7
             T_Cases_172
_ -> T__'8866'__178
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_10
v4
        -> case T_Cases_172 -> T_Cases_172
forall a b. a -> b
coe T_Cases_172
v2 of
             C__'8759'__290 T__'8866'__178
v8 T_Cases_172
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_172 -> T__'8866'__178)
-> Any -> Any -> Any -> T__'8866'__178
forall a b. a -> b
coe T_Vec_28 -> T_Fin_10 -> T_Cases_172 -> T__'8866'__178
du_lookupCase_328 (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_172 -> Any
forall a b. a -> b
coe T_Cases_172
v9)
                    T_Vec_28
_ -> T__'8866'__178
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_Cases_172
_ -> T__'8866'__178
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Fin_10
_ -> T__'8866'__178
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algorithmic.bwdMkCaseType
d_bwdMkCaseType_344 ::
  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_344 :: T_Ctx'8902'_2
-> T_Bwd_6 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
d_bwdMkCaseType_344 ~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_344 T_Bwd_6
v1 T__'8866'Nf'8902'__4
v2
du_bwdMkCaseType_344 ::
  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_344 :: T_Bwd_6 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
du_bwdMkCaseType_344 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''_356 ::
  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''_356 :: T_Ctx'8902'_2
-> T__'8866'Nf'8902'__4 -> [T__'8866'Nf'8902'__4] -> T__'8801'__12
d_lemma'45'bwdfwdfunction''_356 = 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_382 ::
  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_382 :: 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_382 = 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''_410 ::
  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''_410 :: 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''_410 = 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