{-# 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.Type.BetaNBE 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.Data.Fin.Base
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Data.Vec.Base
import qualified MAlonzo.Code.Type
import qualified MAlonzo.Code.Type.BetaNormal
import qualified MAlonzo.Code.Utils

-- Type.BetaNBE.Val
d_Val_4 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 -> ()
d_Val_4 :: T_Ctx'8902'_2 -> T_Kind_476 -> ()
d_Val_4 = T_Ctx'8902'_2 -> T_Kind_476 -> ()
forall a. a
erased
-- Type.BetaNBE.reflect
d_reflect_22 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Ne'8902'__6 -> AgdaAny
d_reflect_22 :: T_Ctx'8902'_2 -> T_Kind_476 -> T__'8866'Ne'8902'__6 -> AgdaAny
d_reflect_22 ~T_Ctx'8902'_2
v0 T_Kind_476
v1 T__'8866'Ne'8902'__6
v2 = T_Kind_476 -> T__'8866'Ne'8902'__6 -> AgdaAny
du_reflect_22 T_Kind_476
v1 T__'8866'Ne'8902'__6
v2
du_reflect_22 ::
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Ne'8902'__6 -> AgdaAny
du_reflect_22 :: T_Kind_476 -> T__'8866'Ne'8902'__6 -> AgdaAny
du_reflect_22 T_Kind_476
v0 T__'8866'Ne'8902'__6
v1
  = case T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v0 of
      T_Kind_476
MAlonzo.Code.Utils.C_'42'_478
        -> (T__'8866'Ne'8902'__6 -> T__'8866'Nf'8902'__4)
-> T__'8866'Ne'8902'__6 -> AgdaAny
forall a b. a -> b
coe T__'8866'Ne'8902'__6 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_ne_20 T__'8866'Ne'8902'__6
v1
      T_Kind_476
MAlonzo.Code.Utils.C_'9839'_480
        -> (T__'8866'Ne'8902'__6 -> T__'8866'Nf'8902'__4)
-> T__'8866'Ne'8902'__6 -> AgdaAny
forall a b. a -> b
coe T__'8866'Ne'8902'__6 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_ne_20 T__'8866'Ne'8902'__6
v1
      MAlonzo.Code.Utils.C__'8658'__482 T_Kind_476
v2 T_Kind_476
v3
        -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 (T__'8866'Ne'8902'__6 -> AgdaAny
forall a b. a -> b
coe T__'8866'Ne'8902'__6
v1)
      T_Kind_476
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNBE.fresh
d_fresh_38 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 -> AgdaAny
d_fresh_38 :: T_Ctx'8902'_2 -> T_Kind_476 -> AgdaAny
d_fresh_38 ~T_Ctx'8902'_2
v0 T_Kind_476
v1 = T_Kind_476 -> AgdaAny
du_fresh_38 T_Kind_476
v1
du_fresh_38 :: MAlonzo.Code.Utils.T_Kind_476 -> AgdaAny
du_fresh_38 :: T_Kind_476 -> AgdaAny
du_fresh_38 T_Kind_476
v0
  = (T_Kind_476 -> T__'8866'Ne'8902'__6 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Kind_476 -> T__'8866'Ne'8902'__6 -> AgdaAny
du_reflect_22 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v0)
      ((T__'8715''8902'__14 -> T__'8866'Ne'8902'__6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T__'8715''8902'__14 -> T__'8866'Ne'8902'__6
MAlonzo.Code.Type.BetaNormal.C_'96'_8
         (T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T__'8715''8902'__14
MAlonzo.Code.Type.C_Z_16))
-- Type.BetaNBE.renVal
d_renVal_46 ::
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8715''8902'__14) ->
  AgdaAny -> AgdaAny
d_renVal_46 :: T_Kind_476
-> T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> AgdaAny
-> AgdaAny
d_renVal_46 T_Kind_476
v0 T_Ctx'8902'_2
v1 T_Ctx'8902'_2
v2 T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v3 AgdaAny
v4
  = case T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v0 of
      T_Kind_476
MAlonzo.Code.Utils.C_'42'_478
        -> (T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
 -> T_Kind_476
 -> T__'8866'Nf'8902'__4
 -> T__'8866'Nf'8902'__4)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.d_renNf_46 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v2) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v3)
             (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)
      T_Kind_476
MAlonzo.Code.Utils.C_'9839'_480
        -> (T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
 -> T_Kind_476
 -> T__'8866'Nf'8902'__4
 -> T__'8866'Nf'8902'__4)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.d_renNf_46 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v2) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v3)
             (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)
      MAlonzo.Code.Utils.C__'8658'__482 T_Kind_476
v5 T_Kind_476
v6
        -> case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
v4 of
             MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v7
               -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
                    ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
 -> T_Kind_476
 -> T__'8866'Ne'8902'__6
 -> T__'8866'Ne'8902'__6)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Ne'8902'__6
-> T__'8866'Ne'8902'__6
MAlonzo.Code.Type.BetaNormal.d_renNe_48 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v2) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v3)
                       (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7))
             MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v7
               -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
                    ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                       (\ AgdaAny
v8 AgdaAny
v9 -> AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7 AgdaAny
v8 (\ AgdaAny
v10 AgdaAny
v11 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v9 AgdaAny
v10 ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v3 AgdaAny
v10 AgdaAny
v11))))
             T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Kind_476
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNBE.weakenVal
d_weakenVal_80 ::
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 -> AgdaAny -> AgdaAny
d_weakenVal_80 :: T_Kind_476 -> T_Ctx'8902'_2 -> T_Kind_476 -> AgdaAny -> AgdaAny
d_weakenVal_80 T_Kind_476
v0 T_Ctx'8902'_2
v1 T_Kind_476
v2
  = (T_Kind_476
 -> T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Kind_476
-> T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> AgdaAny
-> AgdaAny
d_renVal_46 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v0) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1)
      ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> AgdaAny
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 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v2))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v3 -> (T__'8715''8902'__14 -> T__'8715''8902'__14) -> AgdaAny
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8715''8902'__14
MAlonzo.Code.Type.C_S_18))
-- Type.BetaNBE.reify
d_reify_86 ::
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  AgdaAny -> MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
d_reify_86 :: T_Kind_476 -> T_Ctx'8902'_2 -> AgdaAny -> T__'8866'Nf'8902'__4
d_reify_86 T_Kind_476
v0 T_Ctx'8902'_2
v1 AgdaAny
v2
  = case T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v0 of
      T_Kind_476
MAlonzo.Code.Utils.C_'42'_478 -> AgdaAny -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe AgdaAny
v2
      T_Kind_476
MAlonzo.Code.Utils.C_'9839'_480 -> AgdaAny -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe AgdaAny
v2
      MAlonzo.Code.Utils.C__'8658'__482 T_Kind_476
v3 T_Kind_476
v4
        -> case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
v2 of
             MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v5
               -> (T__'8866'Ne'8902'__6 -> T__'8866'Nf'8902'__4)
-> AgdaAny -> 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 AgdaAny
v5
             MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v5
               -> (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4)
-> T__'8866'Nf'8902'__4 -> 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_ƛ_18
                    (T_Kind_476 -> T_Ctx'8902'_2 -> AgdaAny -> T__'8866'Nf'8902'__4
d_reify_86
                       (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v4) ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> 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 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v3))
                       (AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          AgdaAny
v5 ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> AgdaAny
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 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v3))
                          (\ AgdaAny
v6 -> (T__'8715''8902'__14 -> T__'8715''8902'__14) -> AgdaAny
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8715''8902'__14
MAlonzo.Code.Type.C_S_18) ((T_Kind_476 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> AgdaAny
du_fresh_38 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v3))))
             T__'8846'__30
_ -> T__'8866'Nf'8902'__4
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Kind_476
_ -> T__'8866'Nf'8902'__4
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNBE.Env
d_Env_104 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 -> ()
d_Env_104 :: T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> ()
d_Env_104 = T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> ()
forall a. a
erased
-- Type.BetaNBE._,,⋆_
d__'44''44''8902'__122 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  AgdaAny ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny
d__'44''44''8902'__122 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476
-> AgdaAny
-> T_Kind_476
-> T__'8715''8902'__14
-> AgdaAny
d__'44''44''8902'__122 ~T_Ctx'8902'_2
v0 ~T_Ctx'8902'_2
v1 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v2 ~T_Kind_476
v3 AgdaAny
v4 T_Kind_476
v5 T__'8715''8902'__14
v6
  = (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
du__'44''44''8902'__122 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v2 AgdaAny
v4 T_Kind_476
v5 T__'8715''8902'__14
v6
du__'44''44''8902'__122 ::
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  AgdaAny ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny
du__'44''44''8902'__122 :: (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
du__'44''44''8902'__122 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v0 AgdaAny
v1 T_Kind_476
v2 T__'8715''8902'__14
v3
  = case T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe T__'8715''8902'__14
v3 of
      T__'8715''8902'__14
MAlonzo.Code.Type.C_Z_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
      MAlonzo.Code.Type.C_S_18 T__'8715''8902'__14
v7 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v0 T_Kind_476
v2 T__'8715''8902'__14
v7
      T__'8715''8902'__14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNBE.exte
d_exte_140 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny
d_exte_140 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476
-> T_Kind_476
-> T__'8715''8902'__14
-> AgdaAny
d_exte_140 ~T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v2 T_Kind_476
v3 T_Kind_476
v4 = T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476
-> T_Kind_476
-> T__'8715''8902'__14
-> AgdaAny
du_exte_140 T_Ctx'8902'_2
v1 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v2 T_Kind_476
v3 T_Kind_476
v4
du_exte_140 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny
du_exte_140 :: T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476
-> T_Kind_476
-> T__'8715''8902'__14
-> AgdaAny
du_exte_140 T_Ctx'8902'_2
v0 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v1 T_Kind_476
v2 T_Kind_476
v3
  = ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny -> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe
      (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
du__'44''44''8902'__122
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v4 AgdaAny
v5 -> (T_Kind_476 -> T_Ctx'8902'_2 -> T_Kind_476 -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Ctx'8902'_2 -> T_Kind_476 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T_Ctx'8902'_2 -> T_Kind_476 -> AgdaAny -> AgdaAny
d_weakenVal_80 AgdaAny
v4 T_Ctx'8902'_2
v0 T_Kind_476
v2 ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v1 AgdaAny
v4 AgdaAny
v5)))
      ((T_Kind_476 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> AgdaAny
du_fresh_38 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v2)) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v3)
-- Type.BetaNBE._·V_
d__'183'V__150 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny -> AgdaAny
d__'183'V__150 :: T_Ctx'8902'_2
-> T_Kind_476 -> T_Kind_476 -> T__'8846'__30 -> AgdaAny -> AgdaAny
d__'183'V__150 T_Ctx'8902'_2
v0 T_Kind_476
v1 T_Kind_476
v2 T__'8846'__30
v3 AgdaAny
v4
  = case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
      MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v5
        -> (T_Kind_476 -> T__'8866'Ne'8902'__6 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Kind_476 -> T__'8866'Ne'8902'__6 -> AgdaAny
du_reflect_22 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v2)
             ((T_Kind_476
 -> T__'8866'Ne'8902'__6
 -> T__'8866'Nf'8902'__4
 -> T__'8866'Ne'8902'__6)
-> T_Kind_476 -> AgdaAny -> T__'8866'Nf'8902'__4 -> AgdaAny
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 T_Kind_476
v1 AgdaAny
v5
                (T_Kind_476 -> T_Ctx'8902'_2 -> AgdaAny -> T__'8866'Nf'8902'__4
d_reify_86 (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v1) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)))
      MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v5
        -> AgdaAny
-> T_Ctx'8902'_2
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe AgdaAny
v5 T_Ctx'8902'_2
v0 (\ AgdaAny
v6 AgdaAny
v7 -> AgdaAny
v7) AgdaAny
v4
      T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNBE.eval
d_eval_166 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  AgdaAny
d_eval_166 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
d_eval_166 T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 T_Kind_476
v2 T__'8866''8902'__20
v3 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4
  = case T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8866''8902'__20
v3 of
      MAlonzo.Code.Type.C_'96'_22 T__'8715''8902'__14
v7 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4 T_Kind_476
v2 T__'8715''8902'__14
v7
      MAlonzo.Code.Type.C_Π_24 T_Kind_476
v6 T__'8866''8902'__20
v7
        -> (T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4)
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> AgdaAny
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
v6
             (T_Kind_476 -> T_Ctx'8902'_2 -> AgdaAny -> T__'8866'Nf'8902'__4
d_reify_86
                (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)
                ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> 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 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v6))
                ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
d_eval_166
                   ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> AgdaAny
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 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v6))
                   ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> AgdaAny
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 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v6))
                   (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478) (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v7)
                   ((T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> T_Kind_476
 -> T_Kind_476
 -> T__'8715''8902'__14
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476
-> T_Kind_476
-> T__'8715''8902'__14
-> AgdaAny
du_exte_140 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v6))))
      MAlonzo.Code.Type.C__'8658'__26 T__'8866''8902'__20
v6 T__'8866''8902'__20
v7
        -> (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 -> AgdaAny
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_Kind_476 -> T_Ctx'8902'_2 -> AgdaAny -> T__'8866'Nf'8902'__4
d_reify_86
                (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
                ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
d_eval_166 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)
                   (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v6) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4)))
             (T_Kind_476 -> T_Ctx'8902'_2 -> AgdaAny -> T__'8866'Nf'8902'__4
d_reify_86
                (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
                ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
d_eval_166 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)
                   (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v7) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4)))
      MAlonzo.Code.Type.C_ƛ_28 T__'8866''8902'__20
v8
        -> case T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v2 of
             MAlonzo.Code.Utils.C__'8658'__482 T_Kind_476
v9 T_Kind_476
v10
               -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
                    ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                       (\ AgdaAny
v11 AgdaAny
v12 AgdaAny
v13 ->
                          T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
d_eval_166
                            (AgdaAny -> T_Ctx'8902'_2
forall a b. a -> b
coe AgdaAny
v11)
                            ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> 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 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v9))
                            (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v10) (T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8866''8902'__20
v8)
                            (((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny -> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Kind_476
-> T__'8715''8902'__14
-> AgdaAny
forall a b. a -> b
coe
                               (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
du__'44''44''8902'__122
                               ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                                  (\ AgdaAny
v14 AgdaAny
v15 ->
                                     T_Kind_476
-> T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> AgdaAny
-> AgdaAny
d_renVal_46
                                       (AgdaAny -> T_Kind_476
forall a b. a -> b
coe AgdaAny
v14) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (AgdaAny -> T_Ctx'8902'_2
forall a b. a -> b
coe AgdaAny
v11) (AgdaAny -> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe AgdaAny
v12) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4 AgdaAny
v14 AgdaAny
v15)))
                               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v13))))
             T_Kind_476
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Type.C__'183'__30 T_Kind_476
v6 T__'8866''8902'__20
v8 T__'8866''8902'__20
v9
        -> (T_Ctx'8902'_2
 -> T_Kind_476 -> T_Kind_476 -> T__'8846'__30 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Ctx'8902'_2
-> T_Kind_476 -> T_Kind_476 -> T__'8846'__30 -> AgdaAny -> AgdaAny
d__'183'V__150 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v6) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v2)
             ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
d_eval_166 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1)
                ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v6) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v2)) (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v8)
                ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4))
             ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
d_eval_166 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v6) (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v9) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4))
      MAlonzo.Code.Type.C_μ_32 T_Kind_476
v6 T__'8866''8902'__20
v7 T__'8866''8902'__20
v8
        -> (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
-> AgdaAny
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
v6
             (T_Kind_476 -> T_Ctx'8902'_2 -> AgdaAny -> T__'8866'Nf'8902'__4
d_reify_86
                ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> AgdaAny -> AgdaAny -> 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)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v6)
                      (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478))
                   ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v6)
                      (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)))
                (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
                ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
d_eval_166 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1)
                   ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> AgdaAny -> AgdaAny -> AgdaAny
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)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v6)
                         (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478))
                      ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v6)
                         (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)))
                   (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v7) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4)))
             (T_Kind_476 -> T_Ctx'8902'_2 -> AgdaAny -> T__'8866'Nf'8902'__4
d_reify_86
                (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v6) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
                ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
d_eval_166 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v6) (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v8) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4)))
      MAlonzo.Code.Type.C_'94'_34 T_TyCon_6
v7
        -> (T_Kind_476 -> T__'8866'Ne'8902'__6 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Kind_476 -> T__'8866'Ne'8902'__6 -> AgdaAny
du_reflect_22 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v2)
             ((T_TyCon_6 -> T__'8866'Ne'8902'__6) -> T_TyCon_6 -> AgdaAny
forall a b. a -> b
coe T_TyCon_6 -> T__'8866'Ne'8902'__6
MAlonzo.Code.Type.BetaNormal.C_'94'_12 T_TyCon_6
v7)
      MAlonzo.Code.Type.C_con_36 T__'8866''8902'__20
v6
        -> (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_con_22
             (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
d_eval_166
                (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'9839'_480) (T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8866''8902'__20
v6)
                ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4))
      MAlonzo.Code.Type.C_SOP_40 Integer
v6 T_Vec_28
v7
        -> (Integer -> T_Vec_28 -> T__'8866'Nf'8902'__4)
-> Integer -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             Integer -> T_Vec_28 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_SOP_28 Integer
v6
             ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T_Vec_28
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> T_Vec_28)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T_Vec_28
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Vec_28
du_eval'45'VecList_184 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1)
                (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478) (T_Vec_28 -> AgdaAny
forall a b. a -> b
coe T_Vec_28
v7) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4))
      T__'8866''8902'__20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNBE.eval-List
d_eval'45'List_174 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  [MAlonzo.Code.Type.T__'8866''8902'__20] ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  [AgdaAny]
d_eval'45'List_174 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> [T__'8866''8902'__20]
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> [AgdaAny]
d_eval'45'List_174 T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 T_Kind_476
v2 [T__'8866''8902'__20]
v3 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4
  = case [T__'8866''8902'__20] -> [AgdaAny]
forall a b. a -> b
coe [T__'8866''8902'__20]
v3 of
      [] -> [T__'8866''8902'__20] -> [AgdaAny]
forall a b. a -> b
coe [T__'8866''8902'__20]
v3
      (:) AgdaAny
v5 [AgdaAny]
v6
        -> (AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> [AgdaAny]
forall a b. a -> b
coe
             AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
             ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
d_eval_166 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4))
             ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> [T__'8866''8902'__20]
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> [T__'8866''8902'__20]
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> [AgdaAny]
d_eval'45'List_174 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v6) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4))
      [AgdaAny]
_ -> [AgdaAny]
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNBE.eval-VecList
d_eval'45'VecList_184 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  Integer ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28
d_eval'45'VecList_184 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> Integer
-> T_Vec_28
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Vec_28
d_eval'45'VecList_184 T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 T_Kind_476
v2 ~Integer
v3 T_Vec_28
v4 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5
  = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T_Vec_28
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Vec_28
du_eval'45'VecList_184 T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 T_Kind_476
v2 T_Vec_28
v4 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5
du_eval'45'VecList_184 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28
du_eval'45'VecList_184 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T_Vec_28
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Vec_28
du_eval'45'VecList_184 T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 T_Kind_476
v2 T_Vec_28
v3 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4
  = case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v3 of
      T_Vec_28
MAlonzo.Code.Data.Vec.Base.C_'91''93'_32 -> T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v3
      MAlonzo.Code.Data.Vec.Base.C__'8759'__38 AgdaAny
v6 T_Vec_28
v7
        -> (AgdaAny -> T_Vec_28 -> T_Vec_28)
-> [AgdaAny] -> AgdaAny -> T_Vec_28
forall a b. a -> b
coe
             AgdaAny -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38
             (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> [T__'8866''8902'__20]
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> [AgdaAny]
d_eval'45'List_174 (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v2) (AgdaAny -> [T__'8866''8902'__20]
forall a b. a -> b
coe AgdaAny
v6) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4))
             ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T_Vec_28
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> T_Vec_28)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T_Vec_28
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Vec_28
du_eval'45'VecList_184 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v2) (T_Vec_28 -> AgdaAny
forall a b. a -> b
coe T_Vec_28
v7)
                ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4))
      T_Vec_28
_ -> T_Vec_28
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNBE.idEnv
d_idEnv_250 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny
d_idEnv_250 :: T_Ctx'8902'_2 -> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
d_idEnv_250 ~T_Ctx'8902'_2
v0 T_Kind_476
v1 T__'8715''8902'__14
v2 = T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
du_idEnv_250 T_Kind_476
v1 T__'8715''8902'__14
v2
du_idEnv_250 ::
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny
du_idEnv_250 :: T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
du_idEnv_250 T_Kind_476
v0 T__'8715''8902'__14
v1
  = (T_Kind_476 -> T__'8866'Ne'8902'__6 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Kind_476 -> T__'8866'Ne'8902'__6 -> AgdaAny
du_reflect_22 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v0)
      ((T__'8715''8902'__14 -> T__'8866'Ne'8902'__6)
-> T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8866'Ne'8902'__6
MAlonzo.Code.Type.BetaNormal.C_'96'_8 T__'8715''8902'__14
v1)
-- Type.BetaNBE.nf
d_nf_258 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
d_nf_258 :: T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866''8902'__20 -> T__'8866'Nf'8902'__4
d_nf_258 T_Ctx'8902'_2
v0 T_Kind_476
v1 T__'8866''8902'__20
v2
  = (T_Kind_476 -> T_Ctx'8902'_2 -> AgdaAny -> T__'8866'Nf'8902'__4)
-> AgdaAny -> AgdaAny -> AgdaAny -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
      T_Kind_476 -> T_Ctx'8902'_2 -> AgdaAny -> T__'8866'Nf'8902'__4
d_reify_86 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v1) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
      ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
d_eval_166 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v1) (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v2) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
du_idEnv_250))
-- Type.BetaNBE.nf-VecList
d_nf'45'VecList_268 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  Integer ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28
d_nf'45'VecList_268 :: T_Ctx'8902'_2 -> T_Kind_476 -> Integer -> T_Vec_28 -> T_Vec_28
d_nf'45'VecList_268 T_Ctx'8902'_2
v0 T_Kind_476
v1 ~Integer
v2 T_Vec_28
v3 = T_Ctx'8902'_2 -> T_Kind_476 -> T_Vec_28 -> T_Vec_28
du_nf'45'VecList_268 T_Ctx'8902'_2
v0 T_Kind_476
v1 T_Vec_28
v3
du_nf'45'VecList_268 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28
du_nf'45'VecList_268 :: T_Ctx'8902'_2 -> T_Kind_476 -> T_Vec_28 -> T_Vec_28
du_nf'45'VecList_268 T_Ctx'8902'_2
v0 T_Kind_476
v1 T_Vec_28
v2
  = ((AgdaAny -> AgdaAny) -> T_Vec_28 -> T_Vec_28)
-> AgdaAny -> AgdaAny -> T_Vec_28
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_map_178
      (((AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_map_22
         ((T_Kind_476 -> T_Ctx'8902'_2 -> AgdaAny -> T__'8866'Nf'8902'__4)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T_Ctx'8902'_2 -> AgdaAny -> T__'8866'Nf'8902'__4
d_reify_86 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v1) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0)))
      ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T_Vec_28
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> T_Vec_28)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T_Vec_28
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Vec_28
du_eval'45'VecList_184 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v1) (T_Vec_28 -> AgdaAny
forall a b. a -> b
coe T_Vec_28
v2)
         ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
du_idEnv_250))
-- Type.BetaNBE._.lookup-eval-VecList
d_lookup'45'eval'45'VecList_288 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  Integer ->
  MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lookup'45'eval'45'VecList_288 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> Integer
-> T_Fin_10
-> T_Vec_28
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T__'8801'__12
d_lookup'45'eval'45'VecList_288 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> Integer
-> T_Fin_10
-> T_Vec_28
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T__'8801'__12
forall a. a
erased