{-# 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_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
-- Algorithmic.Erasure.eraseTC
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)
-- 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'__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
-- 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'__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
-- 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_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
-- 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_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
-- 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'__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
-- 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'__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
-- 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'__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
-- 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'__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
-- 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'__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
-- 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_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