{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Type.BetaNormal 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.Builtin.Constant.Type
import qualified MAlonzo.Code.Data.Fin.Base
import qualified MAlonzo.Code.Data.Vec.Base
import qualified MAlonzo.Code.Type
import qualified MAlonzo.Code.Type.RenamingSubstitution
import qualified MAlonzo.Code.Utils

-- Type.BetaNormal._⊢Nf⋆_
d__'8866'Nf'8902'__4 :: p -> p -> ()
d__'8866'Nf'8902'__4 p
a0 p
a1 = ()
data T__'8866'Nf'8902'__4
  = C_Π_14 MAlonzo.Code.Utils.T_Kind_476 T__'8866'Nf'8902'__4 |
    C__'8658'__16 T__'8866'Nf'8902'__4 T__'8866'Nf'8902'__4 |
    C_ƛ_18 T__'8866'Nf'8902'__4 | C_ne_20 T__'8866'Ne'8902'__6 |
    C_con_22 T__'8866'Nf'8902'__4 |
    C_μ_24 MAlonzo.Code.Utils.T_Kind_476 T__'8866'Nf'8902'__4
           T__'8866'Nf'8902'__4 |
    C_SOP_28 Integer MAlonzo.Code.Data.Vec.Base.T_Vec_28
-- Type.BetaNormal._⊢Ne⋆_
d__'8866'Ne'8902'__6 :: p -> p -> ()
d__'8866'Ne'8902'__6 p
a0 p
a1 = ()
data T__'8866'Ne'8902'__6
  = C_'96'_8 MAlonzo.Code.Type.T__'8715''8902'__14 |
    C__'183'__10 MAlonzo.Code.Utils.T_Kind_476 T__'8866'Ne'8902'__6
                 T__'8866'Nf'8902'__4 |
    C_'94'_12 MAlonzo.Code.Builtin.Constant.Type.T_TyCon_6
-- Type.BetaNormal.RenNf
d_RenNf_30 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 -> ()
d_RenNf_30 :: T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> ()
d_RenNf_30 = T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> ()
forall a. a
erased
-- Type.BetaNormal.RenNe
d_RenNe_38 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 -> ()
d_RenNe_38 :: T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> ()
d_RenNe_38 = T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> ()
forall a. a
erased
-- Type.BetaNormal.renNf
d_renNf_46 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8715''8902'__14) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
d_renNf_46 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
d_renNf_46 T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2 T_Kind_476
v3 T__'8866'Nf'8902'__4
v4
  = case T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v4 of
      C_Π_14 T_Kind_476
v6 T__'8866'Nf'8902'__4
v7
        -> (T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4)
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
             T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
C_Π_14 T_Kind_476
v6
             (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
d_renNf_46
                ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> Any -> Any -> 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 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v6))
                ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> Any -> Any -> 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 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v6))
                (((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
 -> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> Any -> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
MAlonzo.Code.Type.RenamingSubstitution.du_ext_18 ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14) -> Any
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2))
                (T_Kind_476 -> T_Kind_476
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
v7))
      C__'8658'__16 T__'8866'Nf'8902'__4
v6 T__'8866'Nf'8902'__4
v7
        -> (T__'8866'Nf'8902'__4
 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4)
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
             T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
C__'8658'__16
             (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
d_renNf_46
                (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2) (T_Kind_476 -> T_Kind_476
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
v6))
             (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
d_renNf_46
                (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2) (T_Kind_476 -> T_Kind_476
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
v7))
      C_ƛ_18 T__'8866'Nf'8902'__4
v8
        -> case T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v3 of
             MAlonzo.Code.Utils.C__'8658'__482 T_Kind_476
v9 T_Kind_476
v10
               -> (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4)
-> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
                    T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
C_ƛ_18
                    (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
d_renNf_46
                       ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> Any -> Any -> 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 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9))
                       ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> Any -> Any -> 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 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9))
                       (((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
 -> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> Any -> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
MAlonzo.Code.Type.RenamingSubstitution.du_ext_18 ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14) -> Any
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2))
                       (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v10) (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v8))
             T_Kind_476
_ -> T__'8866'Nf'8902'__4
forall a. a
MAlonzo.RTE.mazUnreachableError
      C_ne_20 T__'8866'Ne'8902'__6
v7
        -> (T__'8866'Ne'8902'__6 -> T__'8866'Nf'8902'__4)
-> T__'8866'Ne'8902'__6 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
             T__'8866'Ne'8902'__6 -> T__'8866'Nf'8902'__4
C_ne_20 (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Ne'8902'__6
-> T__'8866'Ne'8902'__6
d_renNe_48 (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2) (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v3) (T__'8866'Ne'8902'__6 -> T__'8866'Ne'8902'__6
forall a b. a -> b
coe T__'8866'Ne'8902'__6
v7))
      C_con_22 T__'8866'Nf'8902'__4
v6
        -> (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4)
-> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
             T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
C_con_22
             (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
d_renNf_46
                (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2) (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'9839'_480)
                (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v6))
      C_μ_24 T_Kind_476
v6 T__'8866'Nf'8902'__4
v7 T__'8866'Nf'8902'__4
v8
        -> (T_Kind_476
 -> T__'8866'Nf'8902'__4
 -> T__'8866'Nf'8902'__4
 -> T__'8866'Nf'8902'__4)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
             T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
C_μ_24 T_Kind_476
v6
             (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
d_renNf_46
                (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2)
                ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> Any -> Any -> 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) -> Any -> Any -> Any
forall a b. a -> b
coe
                      T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v6)
                      (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478))
                   ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                      T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v6)
                      (T_Kind_476 -> Any
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
v7))
             (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
d_renNf_46 (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2) (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v6) (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v8))
      C_SOP_28 Integer
v6 T_Vec_28
v7
        -> (Integer -> T_Vec_28 -> T__'8866'Nf'8902'__4)
-> Integer -> Any -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
             Integer -> T_Vec_28 -> T__'8866'Nf'8902'__4
C_SOP_28 Integer
v6
             ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
 -> T_Kind_476
 -> T_Vec_28
 -> T_Vec_28)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T_Vec_28
-> T_Vec_28
du_renNf'45'VecList_58 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v1) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14) -> Any
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2)
                (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478) (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v7))
      T__'8866'Nf'8902'__4
_ -> T__'8866'Nf'8902'__4
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNormal.renNe
d_renNe_48 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8715''8902'__14) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  T__'8866'Ne'8902'__6 -> T__'8866'Ne'8902'__6
d_renNe_48 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Ne'8902'__6
-> T__'8866'Ne'8902'__6
d_renNe_48 T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2 T_Kind_476
v3 T__'8866'Ne'8902'__6
v4
  = case T__'8866'Ne'8902'__6 -> T__'8866'Ne'8902'__6
forall a b. a -> b
coe T__'8866'Ne'8902'__6
v4 of
      C_'96'_8 T__'8715''8902'__14
v7 -> (T__'8715''8902'__14 -> T__'8866'Ne'8902'__6)
-> Any -> T__'8866'Ne'8902'__6
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8866'Ne'8902'__6
C_'96'_8 ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476 -> T__'8715''8902'__14 -> Any
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2 T_Kind_476
v3 T__'8715''8902'__14
v7)
      C__'183'__10 T_Kind_476
v6 T__'8866'Ne'8902'__6
v8 T__'8866'Nf'8902'__4
v9
        -> (T_Kind_476
 -> T__'8866'Ne'8902'__6
 -> T__'8866'Nf'8902'__4
 -> T__'8866'Ne'8902'__6)
-> T_Kind_476
-> T__'8866'Ne'8902'__6
-> T__'8866'Nf'8902'__4
-> T__'8866'Ne'8902'__6
forall a b. a -> b
coe
             T_Kind_476
-> T__'8866'Ne'8902'__6
-> T__'8866'Nf'8902'__4
-> T__'8866'Ne'8902'__6
C__'183'__10 T_Kind_476
v6
             (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Ne'8902'__6
-> T__'8866'Ne'8902'__6
d_renNe_48
                (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2)
                ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> Any -> Any -> 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 -> Any
forall a b. a -> b
coe T_Kind_476
v6) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v3)) (T__'8866'Ne'8902'__6 -> T__'8866'Ne'8902'__6
forall a b. a -> b
coe T__'8866'Ne'8902'__6
v8))
             (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
d_renNf_46 (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2) (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v6) (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v9))
      C_'94'_12 T_TyCon_6
v7 -> (T_TyCon_6 -> T__'8866'Ne'8902'__6)
-> T_TyCon_6 -> T__'8866'Ne'8902'__6
forall a b. a -> b
coe T_TyCon_6 -> T__'8866'Ne'8902'__6
C_'94'_12 T_TyCon_6
v7
      T__'8866'Ne'8902'__6
_ -> T__'8866'Ne'8902'__6
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNormal.renNf-List
d_renNf'45'List_52 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8715''8902'__14) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  [T__'8866'Nf'8902'__4] -> [T__'8866'Nf'8902'__4]
d_renNf'45'List_52 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> [T__'8866'Nf'8902'__4]
-> [T__'8866'Nf'8902'__4]
d_renNf'45'List_52 T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2 T_Kind_476
v3 [T__'8866'Nf'8902'__4]
v4
  = case [T__'8866'Nf'8902'__4] -> [Any]
forall a b. a -> b
coe [T__'8866'Nf'8902'__4]
v4 of
      [] -> [T__'8866'Nf'8902'__4] -> [T__'8866'Nf'8902'__4]
forall a b. a -> b
coe [T__'8866'Nf'8902'__4]
v4
      (:) Any
v5 [Any]
v6
        -> (Any -> [Any] -> [Any]) -> Any -> Any -> [T__'8866'Nf'8902'__4]
forall a b. a -> b
coe
             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
             ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
 -> T_Kind_476
 -> T__'8866'Nf'8902'__4
 -> T__'8866'Nf'8902'__4)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
d_renNf_46 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v1) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14) -> Any
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v3) (Any -> Any
forall a b. a -> b
coe Any
v5))
             ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
 -> T_Kind_476
 -> [T__'8866'Nf'8902'__4]
 -> [T__'8866'Nf'8902'__4])
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> [T__'8866'Nf'8902'__4]
-> [T__'8866'Nf'8902'__4]
d_renNf'45'List_52 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v1) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14) -> Any
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v3) ([Any] -> Any
forall a b. a -> b
coe [Any]
v6))
      [Any]
_ -> [T__'8866'Nf'8902'__4]
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNormal.renNf-VecList
d_renNf'45'VecList_58 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  Integer ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8715''8902'__14) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28
d_renNf'45'VecList_58 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> Integer
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T_Vec_28
-> T_Vec_28
d_renNf'45'VecList_58 T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 ~Integer
v2 T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v3 T_Kind_476
v4 T_Vec_28
v5
  = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T_Vec_28
-> T_Vec_28
du_renNf'45'VecList_58 T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v3 T_Kind_476
v4 T_Vec_28
v5
du_renNf'45'VecList_58 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8715''8902'__14) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28
du_renNf'45'VecList_58 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T_Vec_28
-> T_Vec_28
du_renNf'45'VecList_58 T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2 T_Kind_476
v3 T_Vec_28
v4
  = case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v4 of
      T_Vec_28
MAlonzo.Code.Data.Vec.Base.C_'91''93'_32 -> T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v4
      MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v6 T_Vec_28
v7
        -> (Any -> T_Vec_28 -> T_Vec_28)
-> [T__'8866'Nf'8902'__4] -> Any -> T_Vec_28
forall a b. a -> b
coe
             Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38
             (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> [T__'8866'Nf'8902'__4]
-> [T__'8866'Nf'8902'__4]
d_renNf'45'List_52 (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2) (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v3) (Any -> [T__'8866'Nf'8902'__4]
forall a b. a -> b
coe Any
v6))
             ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
 -> T_Kind_476
 -> T_Vec_28
 -> T_Vec_28)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T_Vec_28
-> T_Vec_28
du_renNf'45'VecList_58 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v1) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14) -> Any
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v3)
                (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v7))
      T_Vec_28
_ -> T_Vec_28
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNormal.weakenNf
d_weakenNf_122 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
d_weakenNf_122 :: T_Ctx'8902'_2
-> T_Kind_476
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
d_weakenNf_122 T_Ctx'8902'_2
v0 T_Kind_476
v1 T_Kind_476
v2
  = (T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
 -> T_Kind_476
 -> T__'8866'Nf'8902'__4
 -> T__'8866'Nf'8902'__4)
-> Any
-> Any
-> Any
-> Any
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
      T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
d_renNf_46 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
      ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2) -> Any -> Any -> Any
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 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v2))
      ((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v3 -> (T__'8715''8902'__14 -> T__'8715''8902'__14) -> Any
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8715''8902'__14
MAlonzo.Code.Type.C_S_18)) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v1)
-- Type.BetaNormal.embNf
d_embNf_128 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  T__'8866'Nf'8902'__4 -> MAlonzo.Code.Type.T__'8866''8902'__20
d_embNf_128 :: T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
d_embNf_128 T_Ctx'8902'_2
v0 T_Kind_476
v1 T__'8866'Nf'8902'__4
v2
  = case T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v2 of
      C_Π_14 T_Kind_476
v4 T__'8866'Nf'8902'__4
v5
        -> (T_Kind_476 -> T__'8866''8902'__20 -> T__'8866''8902'__20)
-> T_Kind_476 -> T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe
             T_Kind_476 -> T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_Π_24 T_Kind_476
v4
             (T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
d_embNf_128
                ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> Any -> Any -> 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 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v4))
                (T_Kind_476 -> T_Kind_476
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
v5))
      C__'8658'__16 T__'8866'Nf'8902'__4
v4 T__'8866'Nf'8902'__4
v5
        -> (T__'8866''8902'__20 -> T__'8866''8902'__20 -> T__'8866''8902'__20)
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
forall a b. a -> b
coe
             T__'8866''8902'__20 -> T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C__'8658'__26
             (T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
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
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
v4))
             (T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
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
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
v5))
      C_ƛ_18 T__'8866'Nf'8902'__4
v6
        -> case T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v1 of
             MAlonzo.Code.Utils.C__'8658'__482 T_Kind_476
v7 T_Kind_476
v8
               -> (T__'8866''8902'__20 -> T__'8866''8902'__20)
-> T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe
                    T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_ƛ_28
                    (T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
d_embNf_128
                       ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> Any -> Any -> 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 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v7)) (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v8)
                       (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v6))
             T_Kind_476
_ -> T__'8866''8902'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
      C_ne_20 T__'8866'Ne'8902'__6
v5 -> (T_Ctx'8902'_2 -> T__'8866'Ne'8902'__6 -> T__'8866''8902'__20)
-> Any -> Any -> T__'8866''8902'__20
forall a b. a -> b
coe T_Ctx'8902'_2 -> T__'8866'Ne'8902'__6 -> T__'8866''8902'__20
du_embNe_134 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T__'8866'Ne'8902'__6 -> Any
forall a b. a -> b
coe T__'8866'Ne'8902'__6
v5)
      C_con_22 T__'8866'Nf'8902'__4
v4
        -> (T__'8866''8902'__20 -> T__'8866''8902'__20)
-> T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe
             T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_con_36
             (T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
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
MAlonzo.Code.Utils.C_'9839'_480) (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v4))
      C_μ_24 T_Kind_476
v4 T__'8866'Nf'8902'__4
v5 T__'8866'Nf'8902'__4
v6
        -> (T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
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
v4
             (T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
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)
-> Any -> Any -> 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) -> Any -> Any -> Any
forall a b. a -> b
coe
                      T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v4)
                      (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478))
                   ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                      T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v4)
                      (T_Kind_476 -> Any
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
v5))
             (T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
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
v4) (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v6))
      C_SOP_28 Integer
v4 T_Vec_28
v5
        -> (Integer -> T_Vec_28 -> T__'8866''8902'__20)
-> Integer -> Any -> T__'8866''8902'__20
forall a b. a -> b
coe
             Integer -> T_Vec_28 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_SOP_40 Integer
v4
             ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Vec_28 -> T_Vec_28)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_Ctx'8902'_2 -> T_Kind_476 -> T_Vec_28 -> T_Vec_28
du_embNf'45'VecList_148 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
                (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478) (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v5))
      T__'8866'Nf'8902'__4
_ -> T__'8866''8902'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNormal.embNe
d_embNe_134 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  T__'8866'Ne'8902'__6 -> MAlonzo.Code.Type.T__'8866''8902'__20
d_embNe_134 :: T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Ne'8902'__6 -> T__'8866''8902'__20
d_embNe_134 T_Ctx'8902'_2
v0 ~T_Kind_476
v1 T__'8866'Ne'8902'__6
v2 = T_Ctx'8902'_2 -> T__'8866'Ne'8902'__6 -> T__'8866''8902'__20
du_embNe_134 T_Ctx'8902'_2
v0 T__'8866'Ne'8902'__6
v2
du_embNe_134 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  T__'8866'Ne'8902'__6 -> MAlonzo.Code.Type.T__'8866''8902'__20
du_embNe_134 :: T_Ctx'8902'_2 -> T__'8866'Ne'8902'__6 -> T__'8866''8902'__20
du_embNe_134 T_Ctx'8902'_2
v0 T__'8866'Ne'8902'__6
v1
  = case T__'8866'Ne'8902'__6 -> T__'8866'Ne'8902'__6
forall a b. a -> b
coe T__'8866'Ne'8902'__6
v1 of
      C_'96'_8 T__'8715''8902'__14
v4 -> (T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T__'8715''8902'__14 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'96'_22 T__'8715''8902'__14
v4
      C__'183'__10 T_Kind_476
v3 T__'8866'Ne'8902'__6
v5 T__'8866'Nf'8902'__4
v6
        -> (T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> T_Kind_476 -> Any -> T__'8866''8902'__20 -> T__'8866''8902'__20
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
v3
             ((T_Ctx'8902'_2 -> T__'8866'Ne'8902'__6 -> T__'8866''8902'__20)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Ctx'8902'_2 -> T__'8866'Ne'8902'__6 -> T__'8866''8902'__20
du_embNe_134 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T__'8866'Ne'8902'__6 -> Any
forall a b. a -> b
coe T__'8866'Ne'8902'__6
v5))
             (T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
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
v3) (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v6))
      C_'94'_12 T_TyCon_6
v4 -> (T_TyCon_6 -> T__'8866''8902'__20)
-> T_TyCon_6 -> T__'8866''8902'__20
forall a b. a -> b
coe T_TyCon_6 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'94'_34 T_TyCon_6
v4
      T__'8866'Ne'8902'__6
_ -> T__'8866''8902'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNormal.embNf-List
d_embNf'45'List_140 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  [T__'8866'Nf'8902'__4] -> [MAlonzo.Code.Type.T__'8866''8902'__20]
d_embNf'45'List_140 :: T_Ctx'8902'_2
-> T_Kind_476 -> [T__'8866'Nf'8902'__4] -> [T__'8866''8902'__20]
d_embNf'45'List_140 T_Ctx'8902'_2
v0 T_Kind_476
v1 [T__'8866'Nf'8902'__4]
v2
  = case [T__'8866'Nf'8902'__4] -> [Any]
forall a b. a -> b
coe [T__'8866'Nf'8902'__4]
v2 of
      [] -> [T__'8866'Nf'8902'__4] -> [T__'8866''8902'__20]
forall a b. a -> b
coe [T__'8866'Nf'8902'__4]
v2
      (:) Any
v3 [Any]
v4
        -> (Any -> [Any] -> [Any]) -> Any -> Any -> [T__'8866''8902'__20]
forall a b. a -> b
coe
             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
             ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
d_embNf_128 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v1) (Any -> Any
forall a b. a -> b
coe Any
v3))
             ((T_Ctx'8902'_2
 -> T_Kind_476 -> [T__'8866'Nf'8902'__4] -> [T__'8866''8902'__20])
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
-> T_Kind_476 -> [T__'8866'Nf'8902'__4] -> [T__'8866''8902'__20]
d_embNf'45'List_140 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v1) ([Any] -> Any
forall a b. a -> b
coe [Any]
v4))
      [Any]
_ -> [T__'8866''8902'__20]
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNormal.embNf-VecList
d_embNf'45'VecList_148 ::
  Integer ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28
d_embNf'45'VecList_148 :: Integer -> T_Ctx'8902'_2 -> T_Kind_476 -> T_Vec_28 -> T_Vec_28
d_embNf'45'VecList_148 ~Integer
v0 T_Ctx'8902'_2
v1 T_Kind_476
v2 T_Vec_28
v3
  = T_Ctx'8902'_2 -> T_Kind_476 -> T_Vec_28 -> T_Vec_28
du_embNf'45'VecList_148 T_Ctx'8902'_2
v1 T_Kind_476
v2 T_Vec_28
v3
du_embNf'45'VecList_148 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28
du_embNf'45'VecList_148 :: T_Ctx'8902'_2 -> T_Kind_476 -> T_Vec_28 -> T_Vec_28
du_embNf'45'VecList_148 T_Ctx'8902'_2
v0 T_Kind_476
v1 T_Vec_28
v2
  = case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v2 of
      T_Vec_28
MAlonzo.Code.Data.Vec.Base.C_'91''93'_32 -> T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v2
      MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v4 T_Vec_28
v5
        -> (Any -> T_Vec_28 -> T_Vec_28)
-> [T__'8866''8902'__20] -> Any -> T_Vec_28
forall a b. a -> b
coe
             Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38
             (T_Ctx'8902'_2
-> T_Kind_476 -> [T__'8866'Nf'8902'__4] -> [T__'8866''8902'__20]
d_embNf'45'List_140 (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
v1) (Any -> [T__'8866'Nf'8902'__4]
forall a b. a -> b
coe Any
v4))
             ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Vec_28 -> T_Vec_28)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Kind_476 -> T_Vec_28 -> T_Vec_28
du_embNf'45'VecList_148 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v1) (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v5))
      T_Vec_28
_ -> T_Vec_28
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNormal.ren-embNf
d_ren'45'embNf_190 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8715''8902'__14) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_ren'45'embNf_190 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
d_ren'45'embNf_190 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNormal.ren-embNe
d_ren'45'embNe_198 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8715''8902'__14) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  T__'8866'Ne'8902'__6 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_ren'45'embNe_198 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Ne'8902'__6
-> T__'8801'__12
d_ren'45'embNe_198 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Ne'8902'__6
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNormal.ren-embNf-List
d_ren'45'embNf'45'List_206 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8715''8902'__14) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  [T__'8866'Nf'8902'__4] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_ren'45'embNf'45'List_206 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> [T__'8866'Nf'8902'__4]
-> T__'8801'__12
d_ren'45'embNf'45'List_206 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> [T__'8866'Nf'8902'__4]
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNormal.ren-embNf-VecList
d_ren'45'embNf'45'VecList_216 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8715''8902'__14) ->
  Integer ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_ren'45'embNf'45'VecList_216 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> Integer
-> T_Kind_476
-> T_Vec_28
-> T__'8801'__12
d_ren'45'embNf'45'VecList_216 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> Integer
-> T_Kind_476
-> T_Vec_28
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNormal._.lookup-renNf-VecList
d_lookup'45'renNf'45'VecList_296 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  Integer ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8715''8902'__14) ->
  MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lookup'45'renNf'45'VecList_296 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> Integer
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Fin_10
-> T_Vec_28
-> T__'8801'__12
d_lookup'45'renNf'45'VecList_296 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> Integer
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Fin_10
-> T_Vec_28
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNormal._.lookup-embNf-VecList
d_lookup'45'embNf'45'VecList_312 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  Integer ->
  MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lookup'45'embNf'45'VecList_312 :: T_Ctx'8902'_2 -> Integer -> T_Fin_10 -> T_Vec_28 -> T__'8801'__12
d_lookup'45'embNf'45'VecList_312 = T_Ctx'8902'_2 -> Integer -> T_Fin_10 -> T_Vec_28 -> T__'8801'__12
forall a. a
erased