{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wno-overlapping-patterns #-}
module MAlonzo.Code.Algorithmic.Erasure 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.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Algorithmic
import qualified MAlonzo.Code.Builtin
import qualified MAlonzo.Code.Data.Fin.Base
import qualified MAlonzo.Code.Data.Vec.Base
import qualified MAlonzo.Code.Declarative
import qualified MAlonzo.Code.RawU
import qualified MAlonzo.Code.Type
import qualified MAlonzo.Code.Type.BetaNBE
import qualified MAlonzo.Code.Type.BetaNormal
import qualified MAlonzo.Code.Untyped
import qualified MAlonzo.Code.Utils
import qualified MAlonzo.Code.Utils.List
d_len'8902'_4 :: MAlonzo.Code.Type.T_Ctx'8902'_2 -> ()
d_len'8902'_4 :: T_Ctx'8902'_2 -> ()
d_len'8902'_4 = T_Ctx'8902'_2 -> ()
forall a. a
erased
d_len_12 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Algorithmic.T_Ctx_2 -> ()
d_len_12 :: T_Ctx'8902'_2 -> T_Ctx_2 -> ()
d_len_12 = T_Ctx'8902'_2 -> T_Ctx_2 -> ()
forall a. a
erased
d_eraseVar_28 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Algorithmic.T_Ctx_2 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
MAlonzo.Code.Algorithmic.T__'8715'__16 -> AgdaAny
d_eraseVar_28 :: T_Ctx'8902'_2
-> T_Ctx_2 -> T__'8866'Nf'8902'__4 -> T__'8715'__16 -> AgdaAny
d_eraseVar_28 T_Ctx'8902'_2
v0 T_Ctx_2
v1 ~T__'8866'Nf'8902'__4
v2 T__'8715'__16
v3 = T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8715'__16 -> AgdaAny
du_eraseVar_28 T_Ctx'8902'_2
v0 T_Ctx_2
v1 T__'8715'__16
v3
du_eraseVar_28 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Algorithmic.T_Ctx_2 ->
MAlonzo.Code.Algorithmic.T__'8715'__16 -> AgdaAny
du_eraseVar_28 :: T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8715'__16 -> AgdaAny
du_eraseVar_28 T_Ctx'8902'_2
v0 T_Ctx_2
v1 T__'8715'__16
v2
= case T__'8715'__16 -> T__'8715'__16
forall a b. a -> b
coe T__'8715'__16
v2 of
T__'8715'__16
MAlonzo.Code.Algorithmic.C_Z_22
-> Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
MAlonzo.Code.Algorithmic.C_S_30 T__'8715'__16
v7
-> case T_Ctx_2 -> T_Ctx_2
forall a b. a -> b
coe T_Ctx_2
v1 of
MAlonzo.Code.Algorithmic.C__'44'__12 T_Ctx_2
v9 T__'8866'Nf'8902'__4
v10
-> (AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8715'__16 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8715'__16 -> AgdaAny
du_eraseVar_28 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx_2
v9) (T__'8715'__16 -> AgdaAny
forall a b. a -> b
coe T__'8715'__16
v7))
T_Ctx_2
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Algorithmic.C_T_38 T__'8866'Nf'8902'__4
v6 T__'8715'__16
v7
-> case T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0 of
MAlonzo.Code.Type.C__'44''8902'__6 T_Ctx'8902'_2
v8 T_Kind_476
v9
-> case T_Ctx_2 -> T_Ctx_2
forall a b. a -> b
coe T_Ctx_2
v1 of
MAlonzo.Code.Algorithmic.C__'44''8902'__8 T_Ctx_2
v11
-> (T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8715'__16 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8715'__16 -> AgdaAny
du_eraseVar_28 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v8) (T_Ctx_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx_2
v11) (T__'8715'__16 -> AgdaAny
forall a b. a -> b
coe T__'8715'__16
v7)
T_Ctx_2
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Ctx'8902'_2
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8715'__16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_eraseTC_36 ::
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
AgdaAny -> MAlonzo.Code.RawU.T_TmCon_198
d_eraseTC_36 :: T__'8866'Nf'8902'__4 -> AgdaAny -> T_TmCon_198
d_eraseTC_36 T__'8866'Nf'8902'__4
v0 AgdaAny
v1
= (T__'8866''9839'_4 -> AgdaAny -> T_TmCon_198)
-> AgdaAny -> AgdaAny -> T_TmCon_198
forall a b. a -> b
coe
T__'8866''9839'_4 -> AgdaAny -> T_TmCon_198
MAlonzo.Code.RawU.C_tmCon_202
((T__'8866'Nf'8902'__4 -> T__'8866''9839'_4) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'Nf'8902'__4 -> T__'8866''9839'_4
MAlonzo.Code.Algorithmic.d_ty2sty_64 (T__'8866'Nf'8902'__4 -> AgdaAny
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v0)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
d_erase_48 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Algorithmic.T_Ctx_2 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
MAlonzo.Code.Algorithmic.T__'8866'__168 ->
MAlonzo.Code.Untyped.T__'8866'_14
d_erase_48 :: T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'_14
d_erase_48 T_Ctx'8902'_2
v0 T_Ctx_2
v1 T__'8866'Nf'8902'__4
v2 T__'8866'__168
v3
= case T__'8866'__168 -> T__'8866'__168
forall a b. a -> b
coe T__'8866'__168
v3 of
MAlonzo.Code.Algorithmic.C_'96'_174 T__'8715'__16
v5
-> (AgdaAny -> T__'8866'_14) -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
AgdaAny -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18
((T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8715'__16 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8715'__16 -> AgdaAny
du_eraseVar_28 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx_2
v1) (T__'8715'__16 -> AgdaAny
forall a b. a -> b
coe T__'8715'__16
v5))
MAlonzo.Code.Algorithmic.C_ƛ_180 T__'8866'__168
v6
-> case T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v2 of
MAlonzo.Code.Type.BetaNormal.C__'8658'__16 T__'8866'Nf'8902'__4
v8 T__'8866'Nf'8902'__4
v9
-> (T__'8866'_14 -> T__'8866'_14) -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
((T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'_14
d_erase_48 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
((T_Ctx_2 -> T__'8866'Nf'8902'__4 -> T_Ctx_2)
-> T_Ctx_2 -> T__'8866'Nf'8902'__4 -> AgdaAny
forall a b. a -> b
coe T_Ctx_2 -> T__'8866'Nf'8902'__4 -> T_Ctx_2
MAlonzo.Code.Algorithmic.C__'44'__12 T_Ctx_2
v1 T__'8866'Nf'8902'__4
v8) (T__'8866'Nf'8902'__4 -> AgdaAny
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v9) (T__'8866'__168 -> AgdaAny
forall a b. a -> b
coe T__'8866'__168
v6))
T__'8866'Nf'8902'__4
_ -> T__'8866'_14
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Algorithmic.C__'183'__186 T__'8866'Nf'8902'__4
v4 T__'8866'__168
v6 T__'8866'__168
v7
-> (T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
((T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'_14
d_erase_48 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx_2
v1)
((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__'8866'Nf'8902'__4
v4 T__'8866'Nf'8902'__4
v2) (T__'8866'__168 -> AgdaAny
forall a b. a -> b
coe T__'8866'__168
v6))
((T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'_14
d_erase_48 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx_2
v1) (T__'8866'Nf'8902'__4 -> AgdaAny
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v4) (T__'8866'__168 -> AgdaAny
forall a b. a -> b
coe T__'8866'__168
v7))
MAlonzo.Code.Algorithmic.C_Λ_192 T__'8866'__168
v6
-> case T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v2 of
MAlonzo.Code.Type.BetaNormal.C_Π_14 T_Kind_476
v8 T__'8866'Nf'8902'__4
v9
-> (T__'8866'_14 -> T__'8866'_14) -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_delay_26
((T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'_14
d_erase_48
((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
v8))
((T_Ctx_2 -> T_Ctx_2) -> T_Ctx_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx_2 -> T_Ctx_2
MAlonzo.Code.Algorithmic.C__'44''8902'__8 T_Ctx_2
v1) (T__'8866'Nf'8902'__4 -> AgdaAny
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v9)
(T__'8866'__168 -> AgdaAny
forall a b. a -> b
coe T__'8866'__168
v6))
T__'8866'Nf'8902'__4
_ -> T__'8866'_14
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Algorithmic.C__'183''8902'_'47'__202 T_Kind_476
v4 T__'8866'Nf'8902'__4
v6 T__'8866'__168
v7 T__'8866'Nf'8902'__4
v8
-> (T__'8866'_14 -> T__'8866'_14) -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_force_24
((T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'_14
d_erase_48 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx_2
v1)
((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
v4 T__'8866'Nf'8902'__4
v6) (T__'8866'__168 -> AgdaAny
forall a b. a -> b
coe T__'8866'__168
v7))
MAlonzo.Code.Algorithmic.C_wrap_210 T__'8866'__168
v7
-> case T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v2 of
MAlonzo.Code.Type.BetaNormal.C_μ_24 T_Kind_476
v9 T__'8866'Nf'8902'__4
v10 T__'8866'Nf'8902'__4
v11
-> (T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'_14
d_erase_48 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx_2
v1)
((T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866''8902'__20 -> T__'8866'Nf'8902'__4)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866''8902'__20 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNBE.d_nf_258 (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
MAlonzo.Code.Utils.C_'42'_478)
((T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20)
-> T_Kind_476 -> AgdaAny -> T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe
T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.C__'183'__30 T_Kind_476
v9
((T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20)
-> AgdaAny -> T__'8866''8902'__20 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.C__'183'__30
((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
v9)
(T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478))
(T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
MAlonzo.Code.Type.BetaNormal.d_embNf_128
(T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
((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
v9)
(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
v9)
(T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)))
(T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v10))
((T__'8866''8902'__20 -> T__'8866''8902'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_ƛ_28
((T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20)
-> T_Kind_476 -> T__'8866''8902'__20 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.C_μ_32 T_Kind_476
v9
(T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
MAlonzo.Code.Type.BetaNormal.d_embNf_128
((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
v9))
((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
v9)
(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
v9)
(T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)))
((T_Ctx'8902'_2
-> T_Kind_476
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4)
-> T_Ctx'8902'_2
-> AgdaAny
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
T_Ctx'8902'_2
-> T_Kind_476
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.d_weakenNf_122 T_Ctx'8902'_2
v0
((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
v9)
(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
v9)
(T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)))
T_Kind_476
v9 T__'8866'Nf'8902'__4
v10))
((T__'8715''8902'__14 -> T__'8866''8902'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8715''8902'__14 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'96'_22 (T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T__'8715''8902'__14
MAlonzo.Code.Type.C_Z_16)))))
(T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
MAlonzo.Code.Type.BetaNormal.d_embNf_128
(T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v9) (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v11))))
(T__'8866'__168 -> AgdaAny
forall a b. a -> b
coe T__'8866'__168
v7)
T__'8866'Nf'8902'__4
_ -> T__'8866'_14
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Algorithmic.C_unwrap_220 T_Kind_476
v4 T__'8866'Nf'8902'__4
v6 T__'8866'Nf'8902'__4
v7 T__'8866'__168
v8
-> (T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'_14
d_erase_48 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx_2
v1)
((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
v4 T__'8866'Nf'8902'__4
v6 T__'8866'Nf'8902'__4
v7) (T__'8866'__168 -> AgdaAny
forall a b. a -> b
coe T__'8866'__168
v8)
MAlonzo.Code.Algorithmic.C_constr_230 T_Fin_10
v5 [T__'8866'Nf'8902'__4]
v7 T_IList_302
v9
-> (Integer -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
Integer -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_constr_34
((T_Fin_10 -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Fin_10 -> Integer
MAlonzo.Code.Data.Fin.Base.du_toℕ_18 (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
v5))
((T_Ctx'8902'_2
-> T_Ctx_2
-> [T__'8866'Nf'8902'__4]
-> T_IList_302
-> [T__'8866'_14])
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
-> T_Ctx_2
-> [T__'8866'Nf'8902'__4]
-> T_IList_302
-> [T__'8866'_14]
d_erase'45'ConstrArgs_58 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx_2
v1) ([T__'8866'Nf'8902'__4] -> AgdaAny
forall a b. a -> b
coe [T__'8866'Nf'8902'__4]
v7) (T_IList_302 -> AgdaAny
forall a b. a -> b
coe T_IList_302
v9))
MAlonzo.Code.Algorithmic.C_case_242 Integer
v4 T_Vec_28
v5 T__'8866'__168
v7 T_Cases_162
v8
-> (T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
((T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'_14
d_erase_48 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx_2
v1)
((Integer -> T_Vec_28 -> T__'8866'Nf'8902'__4)
-> Integer -> T_Vec_28 -> AgdaAny
forall a b. a -> b
coe Integer -> T_Vec_28 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_SOP_28 Integer
v4 T_Vec_28
v5) (T__'8866'__168 -> AgdaAny
forall a b. a -> b
coe T__'8866'__168
v7))
((T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T_Vec_28
-> T_Cases_162
-> [T__'8866'_14])
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T_Vec_28
-> T_Cases_162
-> [T__'8866'_14]
du_erase'45'Cases_76 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx_2
v1) (T__'8866'Nf'8902'__4 -> AgdaAny
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v2) (T_Vec_28 -> AgdaAny
forall a b. a -> b
coe T_Vec_28
v5) (T_Cases_162 -> AgdaAny
forall a b. a -> b
coe T_Cases_162
v8))
MAlonzo.Code.Algorithmic.C_con_248 T__'8866'Nf'8902'__4
v4 AgdaAny
v6
-> (T_TmCon_198 -> T__'8866'_14) -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
T_TmCon_198 -> T__'8866'_14
MAlonzo.Code.Untyped.C_con_28 ((T__'8866'Nf'8902'__4 -> AgdaAny -> T_TmCon_198)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'Nf'8902'__4 -> AgdaAny -> T_TmCon_198
d_eraseTC_36 (T__'8866'Nf'8902'__4 -> AgdaAny
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))
MAlonzo.Code.Algorithmic.C_builtin_'47'__254 T_Builtin_2
v5
-> (T_Builtin_2 -> T__'8866'_14) -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe T_Builtin_2 -> T__'8866'_14
MAlonzo.Code.Untyped.C_builtin_44 (T_Builtin_2 -> AgdaAny
forall a b. a -> b
coe T_Builtin_2
v5)
T__'8866'__168
MAlonzo.Code.Algorithmic.C_error_258
-> T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
T__'8866'__168
_ -> T__'8866'_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_erase'45'ConstrArgs_58 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Algorithmic.T_Ctx_2 ->
[MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] ->
MAlonzo.Code.Utils.List.T_IList_302 ->
[MAlonzo.Code.Untyped.T__'8866'_14]
d_erase'45'ConstrArgs_58 :: T_Ctx'8902'_2
-> T_Ctx_2
-> [T__'8866'Nf'8902'__4]
-> T_IList_302
-> [T__'8866'_14]
d_erase'45'ConstrArgs_58 T_Ctx'8902'_2
v0 T_Ctx_2
v1 [T__'8866'Nf'8902'__4]
v2 T_IList_302
v3
= case T_IList_302 -> T_IList_302
forall a b. a -> b
coe T_IList_302
v3 of
T_IList_302
MAlonzo.Code.Utils.List.C_'91''93'_308
-> [AgdaAny] -> [T__'8866'_14]
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16
MAlonzo.Code.Utils.List.C__'8759'__314 AgdaAny
v6 T_IList_302
v7
-> case [T__'8866'Nf'8902'__4] -> [AgdaAny]
forall a b. a -> b
coe [T__'8866'Nf'8902'__4]
v2 of
(:) AgdaAny
v8 [AgdaAny]
v9
-> (AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> [T__'8866'_14]
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_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'_14
d_erase_48 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx_2
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v8) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))
((T_Ctx'8902'_2
-> T_Ctx_2
-> [T__'8866'Nf'8902'__4]
-> T_IList_302
-> [T__'8866'_14])
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
-> T_Ctx_2
-> [T__'8866'Nf'8902'__4]
-> T_IList_302
-> [T__'8866'_14]
d_erase'45'ConstrArgs_58 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx_2
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v9) (T_IList_302 -> AgdaAny
forall a b. a -> b
coe T_IList_302
v7))
[AgdaAny]
_ -> [T__'8866'_14]
forall a. a
MAlonzo.RTE.mazUnreachableError
T_IList_302
_ -> [T__'8866'_14]
forall a. a
MAlonzo.RTE.mazUnreachableError
d_erase'45'Cases_76 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Algorithmic.T_Ctx_2 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
Integer ->
MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
MAlonzo.Code.Algorithmic.T_Cases_162 ->
[MAlonzo.Code.Untyped.T__'8866'_14]
d_erase'45'Cases_76 :: T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> Integer
-> T_Vec_28
-> T_Cases_162
-> [T__'8866'_14]
d_erase'45'Cases_76 T_Ctx'8902'_2
v0 T_Ctx_2
v1 T__'8866'Nf'8902'__4
v2 ~Integer
v3 T_Vec_28
v4 T_Cases_162
v5
= T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T_Vec_28
-> T_Cases_162
-> [T__'8866'_14]
du_erase'45'Cases_76 T_Ctx'8902'_2
v0 T_Ctx_2
v1 T__'8866'Nf'8902'__4
v2 T_Vec_28
v4 T_Cases_162
v5
du_erase'45'Cases_76 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Algorithmic.T_Ctx_2 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
MAlonzo.Code.Algorithmic.T_Cases_162 ->
[MAlonzo.Code.Untyped.T__'8866'_14]
du_erase'45'Cases_76 :: T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T_Vec_28
-> T_Cases_162
-> [T__'8866'_14]
du_erase'45'Cases_76 T_Ctx'8902'_2
v0 T_Ctx_2
v1 T__'8866'Nf'8902'__4
v2 T_Vec_28
v3 T_Cases_162
v4
= case T_Cases_162 -> T_Cases_162
forall a b. a -> b
coe T_Cases_162
v4 of
T_Cases_162
MAlonzo.Code.Algorithmic.C_'91''93'_268
-> [AgdaAny] -> [T__'8866'_14]
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16
MAlonzo.Code.Algorithmic.C__'8759'__280 T__'8866'__168
v8 T_Cases_162
v9
-> case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v3 of
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 AgdaAny
v11 T_Vec_28
v12
-> (AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> [T__'8866'_14]
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_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'_14
d_erase_48 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx_2
v1)
((T__'8866'Nf'8902'__4
-> [T__'8866'Nf'8902'__4] -> 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] -> T__'8866'Nf'8902'__4
MAlonzo.Code.Algorithmic.du_mkCaseType_146 T__'8866'Nf'8902'__4
v2 AgdaAny
v11) (T__'8866'__168 -> AgdaAny
forall a b. a -> b
coe T__'8866'__168
v8))
((T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T_Vec_28
-> T_Cases_162
-> [T__'8866'_14])
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T_Vec_28
-> T_Cases_162
-> [T__'8866'_14]
du_erase'45'Cases_76 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx_2
v1) (T__'8866'Nf'8902'__4 -> AgdaAny
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v2) (T_Vec_28 -> AgdaAny
forall a b. a -> b
coe T_Vec_28
v12) (T_Cases_162 -> AgdaAny
forall a b. a -> b
coe T_Cases_162
v9))
T_Vec_28
_ -> [T__'8866'_14]
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Cases_162
_ -> [T__'8866'_14]
forall a. a
MAlonzo.RTE.mazUnreachableError
d_lenLemma_130 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Declarative.T_Ctx_16 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lenLemma_130 :: T_Ctx'8902'_2 -> T_Ctx_16 -> T__'8801'__12
d_lenLemma_130 = T_Ctx'8902'_2 -> T_Ctx_16 -> T__'8801'__12
forall a. a
erased
d_lenLemma'8902'_142 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lenLemma'8902'_142 :: T_Ctx'8902'_2 -> T__'8801'__12
d_lenLemma'8902'_142 = T_Ctx'8902'_2 -> T__'8801'__12
forall a. a
erased
d_lemzero_154 ::
() ->
() ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lemzero_154 :: () -> () -> T__'8801'__12 -> T__'8801'__12
d_lemzero_154 = () -> () -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
d_lemsuc_166 ::
() ->
() ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lemsuc_166 :: ()
-> () -> T__'8801'__12 -> T__'8801'__12 -> AgdaAny -> T__'8801'__12
d_lemsuc_166 = ()
-> () -> T__'8801'__12 -> T__'8801'__12 -> AgdaAny -> T__'8801'__12
forall a. a
erased
d_lem'8801'Ctx_176 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Algorithmic.T_Ctx_2 ->
MAlonzo.Code.Algorithmic.T_Ctx_2 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lem'8801'Ctx_176 :: T_Ctx'8902'_2
-> T_Ctx_2 -> T_Ctx_2 -> T__'8801'__12 -> T__'8801'__12
d_lem'8801'Ctx_176 = T_Ctx'8902'_2
-> T_Ctx_2 -> T_Ctx_2 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
d_lem'45'conv'8715'_194 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Algorithmic.T_Ctx_2 ->
MAlonzo.Code.Algorithmic.T_Ctx_2 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Algorithmic.T__'8715'__16 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lem'45'conv'8715'_194 :: T_Ctx'8902'_2
-> T_Ctx_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
-> T__'8801'__12
-> T__'8715'__16
-> T__'8801'__12
d_lem'45'conv'8715'_194 = T_Ctx'8902'_2
-> T_Ctx_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
-> T__'8801'__12
-> T__'8715'__16
-> T__'8801'__12
forall a. a
erased
d_sameVar_206 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Declarative.T_Ctx_16 ->
MAlonzo.Code.Type.T__'8866''8902'__20 ->
MAlonzo.Code.Declarative.T__'8715'__34 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_sameVar_206 :: T_Ctx'8902'_2
-> T_Ctx_16
-> T__'8866''8902'__20
-> T__'8715'__34
-> T__'8801'__12
d_sameVar_206 = T_Ctx'8902'_2
-> T_Ctx_16
-> T__'8866''8902'__20
-> T__'8715'__34
-> T__'8801'__12
forall a. a
erased
d_lemVar_228 ::
() ->
() ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lemVar_228 :: () -> () -> T__'8801'__12 -> AgdaAny -> T__'8801'__12
d_lemVar_228 = () -> () -> T__'8801'__12 -> AgdaAny -> T__'8801'__12
forall a. a
erased
d_lemƛ_242 ::
() ->
() ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lemƛ_242 :: ()
-> ()
-> T__'8801'__12
-> T__'8801'__12
-> T__'8866'_14
-> T__'8801'__12
d_lemƛ_242 = ()
-> ()
-> T__'8801'__12
-> T__'8801'__12
-> T__'8866'_14
-> T__'8801'__12
forall a. a
erased
d_lem'183'_256 ::
() ->
() ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lem'183'_256 :: ()
-> ()
-> T__'8801'__12
-> T__'8866'_14
-> T__'8866'_14
-> T__'8801'__12
d_lem'183'_256 = ()
-> ()
-> T__'8801'__12
-> T__'8866'_14
-> T__'8866'_14
-> T__'8801'__12
forall a. a
erased
d_lem'45'delay_270 ::
() ->
() ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lem'45'delay_270 :: () -> () -> T__'8801'__12 -> T__'8866'_14 -> T__'8801'__12
d_lem'45'delay_270 = () -> () -> T__'8801'__12 -> T__'8866'_14 -> T__'8801'__12
forall a. a
erased
d_lem'45'force_282 ::
() ->
() ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lem'45'force_282 :: () -> () -> T__'8801'__12 -> T__'8866'_14 -> T__'8801'__12
d_lem'45'force_282 = () -> () -> T__'8801'__12 -> T__'8866'_14 -> T__'8801'__12
forall a. a
erased
d_lemcon''_294 ::
() ->
() ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.RawU.T_TmCon_198 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lemcon''_294 :: () -> () -> T__'8801'__12 -> T_TmCon_198 -> T__'8801'__12
d_lemcon''_294 = () -> () -> T__'8801'__12 -> T_TmCon_198 -> T__'8801'__12
forall a. a
erased
d_lemerror_304 ::
() ->
() ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lemerror_304 :: () -> () -> T__'8801'__12 -> T__'8801'__12
d_lemerror_304 = () -> () -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
d_lembuiltin_314 ::
() ->
() ->
MAlonzo.Code.Builtin.T_Builtin_2 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lembuiltin_314 :: () -> () -> T_Builtin_2 -> T__'8801'__12 -> T__'8801'__12
d_lembuiltin_314 = () -> () -> T_Builtin_2 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
d_lemConstr_328 ::
() ->
() ->
Integer ->
[MAlonzo.Code.Untyped.T__'8866'_14] ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lemConstr_328 :: ()
-> ()
-> Integer
-> [T__'8866'_14]
-> T__'8801'__12
-> T__'8801'__12
d_lemConstr_328 = ()
-> ()
-> Integer
-> [T__'8866'_14]
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_lemCase_350 ::
() ->
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
[MAlonzo.Code.Untyped.T__'8866'_14] ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lemCase_350 :: ()
-> ()
-> T__'8866'_14
-> [T__'8866'_14]
-> T__'8801'__12
-> T__'8801'__12
d_lemCase_350 = ()
-> ()
-> T__'8866'_14
-> [T__'8866'_14]
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_lem'45'erase_372 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Algorithmic.T_Ctx_2 ->
MAlonzo.Code.Algorithmic.T_Ctx_2 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Algorithmic.T__'8866'__168 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lem'45'erase_372 :: T_Ctx'8902'_2
-> T_Ctx_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
-> T__'8801'__12
-> T__'8866'__168
-> T__'8801'__12
d_lem'45'erase_372 = T_Ctx'8902'_2
-> T_Ctx_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
-> T__'8801'__12
-> T__'8866'__168
-> T__'8801'__12
forall a. a
erased
d_lem'45'subst_382 ::
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lem'45'subst_382 :: () -> T__'8866'_14 -> T__'8801'__12 -> T__'8801'__12
d_lem'45'subst_382 = () -> T__'8866'_14 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
d_lem'45'erase''_398 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Algorithmic.T_Ctx_2 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Algorithmic.T__'8866'__168 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lem'45'erase''_398 :: T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
-> T__'8866'__168
-> T__'8801'__12
d_lem'45'erase''_398 = T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
-> T__'8866'__168
-> T__'8801'__12
forall a. a
erased
d_lem'45'erase''''_420 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Algorithmic.T_Ctx_2 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Algorithmic.T__'8866'__168 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lem'45'erase''''_420 :: T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
-> T__'8866'__168
-> T__'8801'__12
d_lem'45'erase''''_420 = T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
-> T__'8866'__168
-> T__'8801'__12
forall a. a
erased
d_same_432 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Declarative.T_Ctx_16 ->
MAlonzo.Code.Type.T__'8866''8902'__20 ->
MAlonzo.Code.Declarative.T__'8866'__110 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_same_432 :: T_Ctx'8902'_2
-> T_Ctx_16
-> T__'8866''8902'__20
-> T__'8866'__110
-> T__'8801'__12
d_same_432 = T_Ctx'8902'_2
-> T_Ctx_16
-> T__'8866''8902'__20
-> T__'8866'__110
-> T__'8801'__12
forall a. a
erased
d_'43'cancel_442 ::
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'43'cancel_442 :: Integer
-> Integer
-> Integer
-> Integer
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
d_'43'cancel_442 = Integer
-> Integer
-> Integer
-> Integer
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_same'45'ConstrArgs_454 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Declarative.T_Ctx_16 ->
[MAlonzo.Code.Type.T__'8866''8902'__20] ->
MAlonzo.Code.Utils.List.T_IList_302 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_same'45'ConstrArgs_454 :: T_Ctx'8902'_2
-> T_Ctx_16
-> [T__'8866''8902'__20]
-> T_IList_302
-> T__'8801'__12
d_same'45'ConstrArgs_454 = T_Ctx'8902'_2
-> T_Ctx_16
-> [T__'8866''8902'__20]
-> T_IList_302
-> T__'8801'__12
forall a. a
erased
d_same'45'mkCaseType_478 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Algorithmic.T_Ctx_2 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
MAlonzo.Code.Algorithmic.T__'8866'__168 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_same'45'mkCaseType_478 :: T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8801'__12
-> T__'8801'__12
d_same'45'mkCaseType_478 = T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_same'45'Cases_494 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Declarative.T_Ctx_16 ->
MAlonzo.Code.Type.T__'8866''8902'__20 ->
Integer ->
MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
MAlonzo.Code.Declarative.T_Cases_104 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_same'45'Cases_494 :: T_Ctx'8902'_2
-> T_Ctx_16
-> T__'8866''8902'__20
-> Integer
-> T_Vec_28
-> T_Cases_104
-> T__'8801'__12
d_same'45'Cases_494 = T_Ctx'8902'_2
-> T_Ctx_16
-> T__'8866''8902'__20
-> Integer
-> T_Vec_28
-> T_Cases_104
-> T__'8801'__12
forall a. a
erased
d_same''Len_596 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Algorithmic.T_Ctx_2 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_same''Len_596 :: T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8801'__12
d_same''Len_596 = T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8801'__12
forall a. a
erased
d_lem'45'Dconv'8715'_622 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Declarative.T_Ctx_16 ->
MAlonzo.Code.Declarative.T_Ctx_16 ->
MAlonzo.Code.Type.T__'8866''8902'__20 ->
MAlonzo.Code.Type.T__'8866''8902'__20 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Declarative.T__'8715'__34 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lem'45'Dconv'8715'_622 :: T_Ctx'8902'_2
-> T_Ctx_16
-> T_Ctx_16
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8801'__12
-> T__'8801'__12
-> T__'8715'__34
-> T__'8801'__12
d_lem'45'Dconv'8715'_622 = T_Ctx'8902'_2
-> T_Ctx_16
-> T_Ctx_16
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8801'__12
-> T__'8801'__12
-> T__'8715'__34
-> T__'8801'__12
forall a. a
erased
d_same''Var_634 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Algorithmic.T_Ctx_2 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
MAlonzo.Code.Algorithmic.T__'8715'__16 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_same''Var_634 :: T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8715'__16
-> T__'8801'__12
d_same''Var_634 = T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8715'__16
-> T__'8801'__12
forall a. a
erased
d_same''TC_656 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Algorithmic.T_Ctx_2 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_same''TC_656 :: T_Ctx'8902'_2
-> T_Ctx_2 -> T__'8866'Nf'8902'__4 -> AgdaAny -> T__'8801'__12
d_same''TC_656 = T_Ctx'8902'_2
-> T_Ctx_2 -> T__'8866'Nf'8902'__4 -> AgdaAny -> T__'8801'__12
forall a. a
erased
d_same''_674 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Algorithmic.T_Ctx_2 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
MAlonzo.Code.Algorithmic.T__'8866'__168 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_same''_674 :: T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8801'__12
d_same''_674 = T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8801'__12
forall a. a
erased
d_same''ConstrArgs_684 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Algorithmic.T_Ctx_2 ->
[MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] ->
MAlonzo.Code.Utils.List.T_IList_302 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_same''ConstrArgs_684 :: T_Ctx'8902'_2
-> T_Ctx_2
-> [T__'8866'Nf'8902'__4]
-> T_IList_302
-> T__'8801'__12
d_same''ConstrArgs_684 = T_Ctx'8902'_2
-> T_Ctx_2
-> [T__'8866'Nf'8902'__4]
-> T_IList_302
-> T__'8801'__12
forall a. a
erased
d_same'45'subst_702 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Declarative.T_Ctx_16 ->
MAlonzo.Code.Type.T__'8866''8902'__20 ->
MAlonzo.Code.Type.T__'8866''8902'__20 ->
MAlonzo.Code.Declarative.T__'8866'__110 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_same'45'subst_702 :: T_Ctx'8902'_2
-> T_Ctx_16
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866'__110
-> T__'8801'__12
-> T__'8801'__12
d_same'45'subst_702 = T_Ctx'8902'_2
-> T_Ctx_16
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866'__110
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_same''Case_718 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Algorithmic.T_Ctx_2 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
Integer ->
MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
MAlonzo.Code.Algorithmic.T_Cases_162 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_same''Case_718 :: T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> Integer
-> T_Vec_28
-> T_Cases_162
-> T__'8801'__12
d_same''Case_718 = T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> Integer
-> T_Vec_28
-> T_Cases_162
-> T__'8801'__12
forall a. a
erased