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

-- Algorithmic.Erasure.len⋆
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
-- Algorithmic.Erasure.len
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
-- Algorithmic.Erasure.eraseVar
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
-- Algorithmic.Erasure.eraseTC
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)
-- Algorithmic.Erasure.erase
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
-- Algorithmic.Erasure.erase-ConstrArgs
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
-- Algorithmic.Erasure.erase-Cases
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
-- Algorithmic.Erasure.lenLemma
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
-- Algorithmic.Erasure.lenLemma⋆
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
-- Algorithmic.Erasure.lemzero
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
-- Algorithmic.Erasure.lemsuc
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
-- Algorithmic.Erasure.lem≡Ctx
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
-- Algorithmic.Erasure.lem-conv∋
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
-- Algorithmic.Erasure.sameVar
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
-- Algorithmic.Erasure.lemVar
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
-- Algorithmic.Erasure.lemƛ
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
-- Algorithmic.Erasure.lem·
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
-- Algorithmic.Erasure.lem-delay
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
-- Algorithmic.Erasure.lem-force
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
-- Algorithmic.Erasure.lemcon'
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
-- Algorithmic.Erasure.lemerror
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
-- Algorithmic.Erasure.lembuiltin
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
-- Algorithmic.Erasure.lemConstr
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
-- Algorithmic.Erasure.lemCase
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
-- Algorithmic.Erasure.lem-erase
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
-- Algorithmic.Erasure.lem-subst
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
-- Algorithmic.Erasure.lem-erase'
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
-- Algorithmic.Erasure.lem-erase''
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
-- Algorithmic.Erasure.same
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
-- Algorithmic.Erasure.+cancel
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
-- Algorithmic.Erasure.same-ConstrArgs
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
-- Algorithmic.Erasure.same-mkCaseType
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
-- Algorithmic.Erasure.same-Cases
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
-- Algorithmic.Erasure.same'Len
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
-- Algorithmic.Erasure.lem-Dconv∋
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
-- Algorithmic.Erasure.same'Var
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
-- Algorithmic.Erasure.same'TC
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
-- Algorithmic.Erasure.same'
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
-- Algorithmic.Erasure.same'ConstrArgs
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
-- Algorithmic.Erasure.same-subst
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
-- Algorithmic.Erasure.same'Case
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