{-# 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
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
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
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))
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
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))
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
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
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
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)
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
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
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
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
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)
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))
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))
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