{-# 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_652
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_202
d_eraseTC_36 :: T__'8866'Nf'8902'__4 -> AgdaAny -> T_TmCon_202
d_eraseTC_36 T__'8866'Nf'8902'__4
v0 AgdaAny
v1
= (T__'8866''9839'_4 -> AgdaAny -> T_TmCon_202)
-> AgdaAny -> AgdaAny -> T_TmCon_202
forall a b. a -> b
coe
T__'8866''9839'_4 -> AgdaAny -> T_TmCon_202
MAlonzo.Code.RawU.C_tmCon_206
((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'__178 ->
MAlonzo.Code.Untyped.T__'8866'_14
d_erase_48 :: T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__178
-> T__'8866'_14
d_erase_48 T_Ctx'8902'_2
v0 T_Ctx_2
v1 T__'8866'Nf'8902'__4
v2 T__'8866'__178
v3
= case T__'8866'__178 -> T__'8866'__178
forall a b. a -> b
coe T__'8866'__178
v3 of
MAlonzo.Code.Algorithmic.C_'96'_184 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_ƛ_190 T__'8866'__178
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'__178
-> 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'__178
-> 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'__178 -> AgdaAny
forall a b. a -> b
coe T__'8866'__178
v6))
T__'8866'Nf'8902'__4
_ -> T__'8866'_14
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Algorithmic.C__'183'__196 T__'8866'Nf'8902'__4
v4 T__'8866'__178
v6 T__'8866'__178
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'__178
-> 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'__178
-> 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'__178 -> AgdaAny
forall a b. a -> b
coe T__'8866'__178
v6))
((T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__178
-> 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'__178
-> 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'__178 -> AgdaAny
forall a b. a -> b
coe T__'8866'__178
v7))
MAlonzo.Code.Algorithmic.C_Λ_202 T__'8866'__178
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_652
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'__178
-> 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'__178
-> T__'8866'_14
d_erase_48
((T_Ctx'8902'_2 -> T_Kind_652 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Kind_652 -> 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_652 -> AgdaAny
forall a b. a -> b
coe T_Kind_652
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'__178 -> AgdaAny
forall a b. a -> b
coe T__'8866'__178
v6))
T__'8866'Nf'8902'__4
_ -> T__'8866'_14
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Algorithmic.C__'183''8902'_'47'__212 T_Kind_652
v4 T__'8866'Nf'8902'__4
v6 T__'8866'__178
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'__178
-> 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'__178
-> 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_652 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4)
-> T_Kind_652 -> T__'8866'Nf'8902'__4 -> AgdaAny
forall a b. a -> b
coe T_Kind_652 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_Π_14 T_Kind_652
v4 T__'8866'Nf'8902'__4
v6) (T__'8866'__178 -> AgdaAny
forall a b. a -> b
coe T__'8866'__178
v7))
MAlonzo.Code.Algorithmic.C_wrap_220 T__'8866'__178
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_652
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'__178
-> 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'__178
-> 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_652 -> 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_652 -> 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_652 -> AgdaAny
forall a b. a -> b
coe T_Kind_652
MAlonzo.Code.Utils.C_'42'_654)
((T_Kind_652
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20)
-> T_Kind_652 -> AgdaAny -> T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe
T_Kind_652
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.C__'183'__30 T_Kind_652
v9
((T_Kind_652
-> 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_652
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.C__'183'__30
((T_Kind_652 -> T_Kind_652 -> T_Kind_652)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Kind_652 -> T_Kind_652 -> T_Kind_652
MAlonzo.Code.Utils.C__'8658'__658 (T_Kind_652 -> AgdaAny
forall a b. a -> b
coe T_Kind_652
v9)
(T_Kind_652 -> AgdaAny
forall a b. a -> b
coe T_Kind_652
MAlonzo.Code.Utils.C_'42'_654))
(T_Ctx'8902'_2
-> T_Kind_652 -> 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_652 -> T_Kind_652 -> T_Kind_652)
-> AgdaAny -> AgdaAny -> T_Kind_652
forall a b. a -> b
coe
T_Kind_652 -> T_Kind_652 -> T_Kind_652
MAlonzo.Code.Utils.C__'8658'__658
((T_Kind_652 -> T_Kind_652 -> T_Kind_652)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Kind_652 -> T_Kind_652 -> T_Kind_652
MAlonzo.Code.Utils.C__'8658'__658 (T_Kind_652 -> AgdaAny
forall a b. a -> b
coe T_Kind_652
v9)
(T_Kind_652 -> AgdaAny
forall a b. a -> b
coe T_Kind_652
MAlonzo.Code.Utils.C_'42'_654))
((T_Kind_652 -> T_Kind_652 -> T_Kind_652)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Kind_652 -> T_Kind_652 -> T_Kind_652
MAlonzo.Code.Utils.C__'8658'__658 (T_Kind_652 -> AgdaAny
forall a b. a -> b
coe T_Kind_652
v9)
(T_Kind_652 -> AgdaAny
forall a b. a -> b
coe T_Kind_652
MAlonzo.Code.Utils.C_'42'_654)))
(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_652
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20)
-> T_Kind_652 -> T__'8866''8902'__20 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Kind_652
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.C_μ_32 T_Kind_652
v9
(T_Ctx'8902'_2
-> T_Kind_652 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
MAlonzo.Code.Type.BetaNormal.d_embNf_128
((T_Ctx'8902'_2 -> T_Kind_652 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Kind_652 -> 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_652 -> AgdaAny
forall a b. a -> b
coe T_Kind_652
v9))
((T_Kind_652 -> T_Kind_652 -> T_Kind_652)
-> AgdaAny -> AgdaAny -> T_Kind_652
forall a b. a -> b
coe
T_Kind_652 -> T_Kind_652 -> T_Kind_652
MAlonzo.Code.Utils.C__'8658'__658
((T_Kind_652 -> T_Kind_652 -> T_Kind_652)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Kind_652 -> T_Kind_652 -> T_Kind_652
MAlonzo.Code.Utils.C__'8658'__658 (T_Kind_652 -> AgdaAny
forall a b. a -> b
coe T_Kind_652
v9)
(T_Kind_652 -> AgdaAny
forall a b. a -> b
coe T_Kind_652
MAlonzo.Code.Utils.C_'42'_654))
((T_Kind_652 -> T_Kind_652 -> T_Kind_652)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Kind_652 -> T_Kind_652 -> T_Kind_652
MAlonzo.Code.Utils.C__'8658'__658 (T_Kind_652 -> AgdaAny
forall a b. a -> b
coe T_Kind_652
v9)
(T_Kind_652 -> AgdaAny
forall a b. a -> b
coe T_Kind_652
MAlonzo.Code.Utils.C_'42'_654)))
((T_Ctx'8902'_2
-> T_Kind_652
-> T_Kind_652
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4)
-> T_Ctx'8902'_2
-> AgdaAny
-> T_Kind_652
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
T_Ctx'8902'_2
-> T_Kind_652
-> T_Kind_652
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.d_weakenNf_122 T_Ctx'8902'_2
v0
((T_Kind_652 -> T_Kind_652 -> T_Kind_652)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Kind_652 -> T_Kind_652 -> T_Kind_652
MAlonzo.Code.Utils.C__'8658'__658
((T_Kind_652 -> T_Kind_652 -> T_Kind_652)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Kind_652 -> T_Kind_652 -> T_Kind_652
MAlonzo.Code.Utils.C__'8658'__658 (T_Kind_652 -> AgdaAny
forall a b. a -> b
coe T_Kind_652
v9)
(T_Kind_652 -> AgdaAny
forall a b. a -> b
coe T_Kind_652
MAlonzo.Code.Utils.C_'42'_654))
((T_Kind_652 -> T_Kind_652 -> T_Kind_652)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Kind_652 -> T_Kind_652 -> T_Kind_652
MAlonzo.Code.Utils.C__'8658'__658 (T_Kind_652 -> AgdaAny
forall a b. a -> b
coe T_Kind_652
v9)
(T_Kind_652 -> AgdaAny
forall a b. a -> b
coe T_Kind_652
MAlonzo.Code.Utils.C_'42'_654)))
T_Kind_652
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_652 -> 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_652 -> T_Kind_652
forall a b. a -> b
coe T_Kind_652
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'__178 -> AgdaAny
forall a b. a -> b
coe T__'8866'__178
v7)
T__'8866'Nf'8902'__4
_ -> T__'8866'_14
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Algorithmic.C_unwrap_230 T_Kind_652
v4 T__'8866'Nf'8902'__4
v6 T__'8866'Nf'8902'__4
v7 T__'8866'__178
v8
-> (T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__178
-> 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'__178
-> 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_652
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4)
-> T_Kind_652
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> AgdaAny
forall a b. a -> b
coe T_Kind_652
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_μ_24 T_Kind_652
v4 T__'8866'Nf'8902'__4
v6 T__'8866'Nf'8902'__4
v7) (T__'8866'__178 -> AgdaAny
forall a b. a -> b
coe T__'8866'__178
v8)
MAlonzo.Code.Algorithmic.C_constr_240 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_252 Integer
v4 T_Vec_28
v5 T__'8866'__178
v7 T_Cases_172
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'__178
-> 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'__178
-> 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'__178 -> AgdaAny
forall a b. a -> b
coe T__'8866'__178
v7))
((T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T_Vec_28
-> T_Cases_172
-> [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_172
-> [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_172 -> AgdaAny
forall a b. a -> b
coe T_Cases_172
v8))
MAlonzo.Code.Algorithmic.C_con_258 T__'8866'Nf'8902'__4
v4 AgdaAny
v6
-> (T_TmCon_202 -> T__'8866'_14) -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
T_TmCon_202 -> T__'8866'_14
MAlonzo.Code.Untyped.C_con_28 ((T__'8866'Nf'8902'__4 -> AgdaAny -> T_TmCon_202)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'Nf'8902'__4 -> AgdaAny -> T_TmCon_202
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'__264 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'__178
MAlonzo.Code.Algorithmic.C_error_268
-> T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
T__'8866'__178
_ -> 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'__178
-> 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'__178
-> 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_172 ->
[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_172
-> [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_172
v5
= T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T_Vec_28
-> T_Cases_172
-> [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_172
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_172 ->
[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_172
-> [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_172
v4
= case T_Cases_172 -> T_Cases_172
forall a b. a -> b
coe T_Cases_172
v4 of
T_Cases_172
MAlonzo.Code.Algorithmic.C_'91''93'_278
-> [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'__290 T__'8866'__178
v8 T_Cases_172
v9
-> case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
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'__178
-> 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'__178
-> 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_156 T__'8866'Nf'8902'__4
v2 AgdaAny
v11) (T__'8866'__178 -> AgdaAny
forall a b. a -> b
coe T__'8866'__178
v8))
((T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T_Vec_28
-> T_Cases_172
-> [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_172
-> [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_172 -> AgdaAny
forall a b. a -> b
coe T_Cases_172
v9))
T_Vec_28
_ -> [T__'8866'_14]
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Cases_172
_ -> [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_202 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lemcon''_294 :: () -> () -> T__'8801'__12 -> T_TmCon_202 -> T__'8801'__12
d_lemcon''_294 = () -> () -> T__'8801'__12 -> T_TmCon_202 -> 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'__178 ->
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'__178
-> 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'__178
-> 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'__178 ->
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'__178
-> 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'__178
-> 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'__178 ->
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'__178
-> 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'__178
-> 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'__178 ->
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'__178
-> 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'__178
-> 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'__178 ->
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'__178
-> T__'8801'__12
d_same''_674 = T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__178
-> 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_172 ->
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_172
-> 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_172
-> T__'8801'__12
forall a. a
erased