{-# 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.Declarative 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.Algorithmic
import qualified MAlonzo.Code.Builtin
import qualified MAlonzo.Code.Builtin.Signature
import qualified MAlonzo.Code.Data.Fin.Base
import qualified MAlonzo.Code.Data.Vec.Base
import qualified MAlonzo.Code.Type
import qualified MAlonzo.Code.Type.BetaNBE
import qualified MAlonzo.Code.Type.Equality
import qualified MAlonzo.Code.Type.RenamingSubstitution
import qualified MAlonzo.Code.Utils
import qualified MAlonzo.Code.Utils.List

-- Declarative._.mkTy
d_mkTy_6 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Builtin.Signature.T__'47'_'8866''8902'_22 ->
  MAlonzo.Code.Type.T__'8866''8902'__20
d_mkTy_6 :: Integer
-> Integer -> T__'47'_'8866''8902'_22 -> T__'8866''8902'__20
d_mkTy_6
  = ((T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
 -> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
 -> (T_Ctx'8902'_2 -> Any -> Any)
 -> Integer
 -> Integer
 -> T__'47'_'8866''8902'_22
 -> Any)
-> Any
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> (Any -> Any -> Any)
-> Integer
-> Integer
-> T__'47'_'8866''8902'_22
-> T__'8866''8902'__20
forall a b. a -> b
coe
      (T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any)
-> Integer
-> Integer
-> T__'47'_'8866''8902'_22
-> Any
MAlonzo.Code.Builtin.Signature.du_mkTy_198 ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 -> Any
v2))
      ((Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 Any
v3 -> (T__'8715''8902'__14 -> T__'8866''8902'__20) -> Any -> Any
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'96'_22 Any
v3))
      (\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 -> (T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> Any -> Any -> Any -> Any
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 Any
v1 Any
v3 Any
v4)
      ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 -> (T_TyCon_6 -> T__'8866''8902'__20) -> Any
forall a b. a -> b
coe T_TyCon_6 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'94'_34))
      (\ Any
v0 Any
v1 -> (T__'8866''8902'__20 -> T__'8866''8902'__20) -> Any -> Any
forall a b. a -> b
coe T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_con_36 Any
v1)
-- Declarative._.sig2type
d_sig2type_8 ::
  MAlonzo.Code.Builtin.Signature.T_Sig_68 ->
  MAlonzo.Code.Type.T__'8866''8902'__20
d_sig2type_8 :: T_Sig_68 -> T__'8866''8902'__20
d_sig2type_8
  = ((T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
 -> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
 -> (T_Ctx'8902'_2 -> Any -> Any)
 -> (T_Ctx'8902'_2 -> Any -> Any -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
 -> T_Sig_68
 -> Any)
-> Any
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> (Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_Sig_68
-> T__'8866''8902'__20
forall a b. a -> b
coe
      (T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> T_Sig_68
-> Any
MAlonzo.Code.Builtin.Signature.du_sig2type_236
      ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 -> Any
v2))
      ((Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 Any
v3 -> (T__'8715''8902'__14 -> T__'8866''8902'__20) -> Any -> Any
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'96'_22 Any
v3))
      (\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 -> (T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> Any -> Any -> Any -> Any
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 Any
v1 Any
v3 Any
v4)
      ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 -> (T_TyCon_6 -> T__'8866''8902'__20) -> Any
forall a b. a -> b
coe T_TyCon_6 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'94'_34))
      (\ Any
v0 Any
v1 -> (T__'8866''8902'__20 -> T__'8866''8902'__20) -> Any -> Any
forall a b. a -> b
coe T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_con_36 Any
v1)
      (\ Any
v0 Any
v1 Any
v2 -> (T__'8866''8902'__20 -> T__'8866''8902'__20 -> T__'8866''8902'__20)
-> Any -> Any -> Any
forall a b. a -> b
coe T__'8866''8902'__20 -> T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C__'8658'__26 Any
v1 Any
v2)
      (\ Any
v0 Any
v1 Any
v2 -> (T_Kind_476 -> T__'8866''8902'__20 -> T__'8866''8902'__20)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Kind_476 -> T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_Π_24 Any
v1 Any
v2)
-- Declarative._.sig2typeΠ
d_sig2typeΠ_10 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  MAlonzo.Code.Type.T__'8866''8902'__20
d_sig2typeΠ_10 :: Integer -> Integer -> T__'8866''8902'__20 -> T__'8866''8902'__20
d_sig2typeΠ_10
  = ((T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
 -> Integer -> Integer -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Integer
-> Integer
-> T__'8866''8902'__20
-> T__'8866''8902'__20
forall a b. a -> b
coe
      (T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> Integer -> Integer -> Any -> Any
MAlonzo.Code.Builtin.Signature.du_sig2typeΠ_222
      (\ Any
v0 Any
v1 Any
v2 -> (T_Kind_476 -> T__'8866''8902'__20 -> T__'8866''8902'__20)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Kind_476 -> T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_Π_24 Any
v1 Any
v2)
-- Declarative._.sig2type⇒
d_sig2type'8658'_12 ::
  Integer ->
  Integer ->
  [MAlonzo.Code.Builtin.Signature.T__'47'_'8866''8902'_22] ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  MAlonzo.Code.Type.T__'8866''8902'__20
d_sig2type'8658'_12 :: Integer
-> Integer
-> [T__'47'_'8866''8902'_22]
-> T__'8866''8902'__20
-> T__'8866''8902'__20
d_sig2type'8658'_12
  = ((T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
 -> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
 -> (T_Ctx'8902'_2 -> Any -> Any)
 -> (T_Ctx'8902'_2 -> Any -> Any -> Any)
 -> Integer
 -> Integer
 -> [T__'47'_'8866''8902'_22]
 -> Any
 -> Any)
-> Any
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> (Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Integer
-> Integer
-> [T__'47'_'8866''8902'_22]
-> T__'8866''8902'__20
-> T__'8866''8902'__20
forall a b. a -> b
coe
      (T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any -> Any)
-> Integer
-> Integer
-> [T__'47'_'8866''8902'_22]
-> Any
-> Any
MAlonzo.Code.Builtin.Signature.du_sig2type'8658'_208
      ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 -> Any
v2))
      ((Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 Any
v3 -> (T__'8715''8902'__14 -> T__'8866''8902'__20) -> Any -> Any
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'96'_22 Any
v3))
      (\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 -> (T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> Any -> Any -> Any -> Any
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 Any
v1 Any
v3 Any
v4)
      ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 -> (T_TyCon_6 -> T__'8866''8902'__20) -> Any
forall a b. a -> b
coe T_TyCon_6 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'94'_34))
      (\ Any
v0 Any
v1 -> (T__'8866''8902'__20 -> T__'8866''8902'__20) -> Any -> Any
forall a b. a -> b
coe T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_con_36 Any
v1)
      (\ Any
v0 Any
v1 Any
v2 -> (T__'8866''8902'__20 -> T__'8866''8902'__20 -> T__'8866''8902'__20)
-> Any -> Any -> Any
forall a b. a -> b
coe T__'8866''8902'__20 -> T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C__'8658'__26 Any
v1 Any
v2)
-- Declarative._.⊢♯2TyNe♯
d_'8866''9839'2TyNe'9839'_14 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
  MAlonzo.Code.Type.T__'8866''8902'__20
d_'8866''9839'2TyNe'9839'_14 :: Integer -> Integer -> T__'8866''9839'_4 -> T__'8866''8902'__20
d_'8866''9839'2TyNe'9839'_14
  = ((T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
 -> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
 -> Integer
 -> Integer
 -> T__'8866''9839'_4
 -> Any)
-> Any
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Integer
-> Integer
-> T__'8866''9839'_4
-> T__'8866''8902'__20
forall a b. a -> b
coe
      (T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
-> Integer
-> Integer
-> T__'8866''9839'_4
-> Any
MAlonzo.Code.Builtin.Signature.du_'8866''9839'2TyNe'9839'_182
      ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 -> Any
v2))
      ((Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 Any
v3 -> (T__'8715''8902'__14 -> T__'8866''8902'__20) -> Any -> Any
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'96'_22 Any
v3))
      (\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 -> (T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> Any -> Any -> Any -> Any
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 Any
v1 Any
v3 Any
v4)
      ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 -> (T_TyCon_6 -> T__'8866''8902'__20) -> Any
forall a b. a -> b
coe T_TyCon_6 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'94'_34))
-- Declarative.Ctx
d_Ctx_16 :: p -> ()
d_Ctx_16 p
a0 = ()
data T_Ctx_16
  = C_'8709'_18 | C__'44''8902'__22 T_Ctx_16 |
    C__'44'__26 T_Ctx_16 MAlonzo.Code.Type.T__'8866''8902'__20
-- Declarative._∋_
d__'8715'__34 :: p -> p -> p -> ()
d__'8715'__34 p
a0 p
a1 p
a2 = ()
data T__'8715'__34
  = C_Z_36 | C_S_38 T__'8715'__34 |
    C_T_40 MAlonzo.Code.Type.T__'8866''8902'__20 T__'8715'__34
-- Declarative.btype
d_btype_42 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Builtin.T_Builtin_2 ->
  MAlonzo.Code.Type.T__'8866''8902'__20
d_btype_42 :: T_Ctx'8902'_2 -> T_Builtin_2 -> T__'8866''8902'__20
d_btype_42 T_Ctx'8902'_2
v0 T_Builtin_2
v1
  = (T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866''8902'__20 -> T__'8866''8902'__20)
-> Any -> Any -> Any -> T__'8866''8902'__20
forall a b. a -> b
coe
      T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.d_sub'8709'_896 (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_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
 -> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
 -> (T_Ctx'8902'_2 -> Any -> Any)
 -> (T_Ctx'8902'_2 -> Any -> Any -> Any)
 -> (T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
 -> T_Sig_68
 -> Any)
-> Any
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> (Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
forall a b. a -> b
coe
         (T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> T_Sig_68
-> Any
MAlonzo.Code.Builtin.Signature.du_sig2type_236
         ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v2 Any
v3 Any
v4 -> Any
v4))
         ((Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v2 Any
v3 Any
v4 Any
v5 -> (T__'8715''8902'__14 -> T__'8866''8902'__20) -> Any -> Any
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'96'_22 Any
v5))
         (\ Any
v2 Any
v3 Any
v4 Any
v5 Any
v6 -> (T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> Any -> Any -> Any -> Any
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 Any
v3 Any
v5 Any
v6)
         ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v2 Any
v3 -> (T_TyCon_6 -> T__'8866''8902'__20) -> Any
forall a b. a -> b
coe T_TyCon_6 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'94'_34))
         (\ Any
v2 Any
v3 -> (T__'8866''8902'__20 -> T__'8866''8902'__20) -> Any -> Any
forall a b. a -> b
coe T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_con_36 Any
v3)
         (\ Any
v2 Any
v3 Any
v4 -> (T__'8866''8902'__20 -> T__'8866''8902'__20 -> T__'8866''8902'__20)
-> Any -> Any -> Any
forall a b. a -> b
coe T__'8866''8902'__20 -> T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C__'8658'__26 Any
v3 Any
v4)
         (\ Any
v2 Any
v3 Any
v4 -> (T_Kind_476 -> T__'8866''8902'__20 -> T__'8866''8902'__20)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Kind_476 -> T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_Π_24 Any
v3 Any
v4)
         ((T_Builtin_2 -> T_Sig_68) -> Any -> Any
forall a b. a -> b
coe T_Builtin_2 -> T_Sig_68
MAlonzo.Code.Builtin.d_signature_278 (T_Builtin_2 -> Any
forall a b. a -> b
coe T_Builtin_2
v1)))
-- Declarative.btype-ren
d_btype'45'ren_50 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Builtin.T_Builtin_2 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8715''8902'__14) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_btype'45'ren_50 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Builtin_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T__'8801'__12
d_btype'45'ren_50 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Builtin_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T__'8801'__12
forall a. a
erased
-- Declarative.btype-sub
d_btype'45'sub_60 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Builtin.T_Builtin_2 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8866''8902'__20) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_btype'45'sub_60 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Builtin_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T__'8801'__12
d_btype'45'sub_60 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Builtin_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T__'8801'__12
forall a. a
erased
-- Declarative.⟦_⟧d
d_'10214'_'10215'd_68 ::
  MAlonzo.Code.Type.T__'8866''8902'__20 -> ()
d_'10214'_'10215'd_68 :: T__'8866''8902'__20 -> ()
d_'10214'_'10215'd_68 = T__'8866''8902'__20 -> ()
forall a. a
erased
-- Declarative.ty2TyTag
d_ty2TyTag_74 ::
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4
d_ty2TyTag_74 :: T__'8866''8902'__20 -> T__'8866''9839'_4
d_ty2TyTag_74 T__'8866''8902'__20
v0
  = (T__'8866'Nf'8902'__4 -> T__'8866''9839'_4)
-> Any -> T__'8866''9839'_4
forall a b. a -> b
coe
      T__'8866'Nf'8902'__4 -> T__'8866''9839'_4
MAlonzo.Code.Algorithmic.d_ty2sty_64
      ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866''8902'__20 -> T__'8866'Nf'8902'__4)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
         T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866''8902'__20 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNBE.d_nf_258
         (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
         (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'9839'_480) (T__'8866''8902'__20 -> Any
forall a b. a -> b
coe T__'8866''8902'__20
v0))
-- Declarative.mkCaseType
d_mkCaseType_82 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  [MAlonzo.Code.Type.T__'8866''8902'__20] ->
  MAlonzo.Code.Type.T__'8866''8902'__20
d_mkCaseType_82 :: T_Ctx'8902'_2
-> T__'8866''8902'__20
-> [T__'8866''8902'__20]
-> T__'8866''8902'__20
d_mkCaseType_82 ~T_Ctx'8902'_2
v0 T__'8866''8902'__20
v1 [T__'8866''8902'__20]
v2 = T__'8866''8902'__20 -> [T__'8866''8902'__20] -> T__'8866''8902'__20
du_mkCaseType_82 T__'8866''8902'__20
v1 [T__'8866''8902'__20]
v2
du_mkCaseType_82 ::
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  [MAlonzo.Code.Type.T__'8866''8902'__20] ->
  MAlonzo.Code.Type.T__'8866''8902'__20
du_mkCaseType_82 :: T__'8866''8902'__20 -> [T__'8866''8902'__20] -> T__'8866''8902'__20
du_mkCaseType_82 T__'8866''8902'__20
v0 [T__'8866''8902'__20]
v1
  = case [T__'8866''8902'__20] -> [Any]
forall a b. a -> b
coe [T__'8866''8902'__20]
v1 of
      [] -> T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8866''8902'__20
v0
      (:) Any
v2 [Any]
v3
        -> (T__'8866''8902'__20 -> T__'8866''8902'__20 -> T__'8866''8902'__20)
-> Any -> Any -> 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 Any
v2
             ((T__'8866''8902'__20
 -> [T__'8866''8902'__20] -> T__'8866''8902'__20)
-> Any -> Any -> Any
forall a b. a -> b
coe T__'8866''8902'__20 -> [T__'8866''8902'__20] -> T__'8866''8902'__20
du_mkCaseType_82 (T__'8866''8902'__20 -> Any
forall a b. a -> b
coe T__'8866''8902'__20
v0) ([Any] -> Any
forall a b. a -> b
coe [Any]
v3))
      [Any]
_ -> T__'8866''8902'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Declarative.ConstrArgs
d_ConstrArgs_94 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  T_Ctx_16 -> [MAlonzo.Code.Type.T__'8866''8902'__20] -> ()
d_ConstrArgs_94 :: T_Ctx'8902'_2 -> T_Ctx_16 -> [T__'8866''8902'__20] -> ()
d_ConstrArgs_94 = T_Ctx'8902'_2 -> T_Ctx_16 -> [T__'8866''8902'__20] -> ()
forall a. a
erased
-- Declarative.Cases
d_Cases_104 :: p -> p -> p -> p -> p -> ()
d_Cases_104 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
data T_Cases_104
  = C_'91''93'_180 | C__'8759'__192 T__'8866'__110 T_Cases_104
-- Declarative._⊢_
d__'8866'__110 :: p -> p -> p -> ()
d__'8866'__110 p
a0 p
a1 p
a2 = ()
data T__'8866'__110
  = C_'96'_114 T__'8715'__34 | C_ƛ_116 T__'8866'__110 |
    C__'183'__118 MAlonzo.Code.Type.T__'8866''8902'__20 T__'8866'__110
                  T__'8866'__110 |
    C_Λ_120 T__'8866'__110 |
    C__'183''8902'__124 MAlonzo.Code.Utils.T_Kind_476
                        MAlonzo.Code.Type.T__'8866''8902'__20 T__'8866'__110
                        MAlonzo.Code.Type.T__'8866''8902'__20 |
    C_wrap_130 T__'8866'__110 | C_unwrap_132 T__'8866'__110 |
    C_constr_142 MAlonzo.Code.Data.Fin.Base.T_Fin_6
                 [MAlonzo.Code.Type.T__'8866''8902'__20]
                 MAlonzo.Code.Utils.List.T_IList_302 |
    C_case_154 Integer MAlonzo.Code.Data.Vec.Base.T_Vec_24
               T__'8866'__110 T_Cases_104 |
    C_conv_156 MAlonzo.Code.Type.T__'8866''8902'__20
               MAlonzo.Code.Type.Equality.T__'8801'β__10 T__'8866'__110 |
    C_con_162 MAlonzo.Code.Type.T__'8866''8902'__20 AgdaAny
              MAlonzo.Code.Type.Equality.T__'8801'β__10 |
    C_builtin_166 MAlonzo.Code.Builtin.T_Builtin_2 | C_error_170
-- Declarative.conv∋
d_conv'8715'_194 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  T_Ctx_16 ->
  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 ->
  T__'8715'__34 -> T__'8715'__34
d_conv'8715'_194 :: 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__'8715'__34
d_conv'8715'_194 ~T_Ctx'8902'_2
v0 ~T_Ctx_16
v1 ~T_Ctx_16
v2 ~T__'8866''8902'__20
v3 ~T__'8866''8902'__20
v4 ~T__'8801'__12
v5 ~T__'8801'__12
v6 T__'8715'__34
v7
  = T__'8715'__34 -> T__'8715'__34
du_conv'8715'_194 T__'8715'__34
v7
du_conv'8715'_194 :: T__'8715'__34 -> T__'8715'__34
du_conv'8715'_194 :: T__'8715'__34 -> T__'8715'__34
du_conv'8715'_194 T__'8715'__34
v0 = T__'8715'__34 -> T__'8715'__34
forall a b. a -> b
coe T__'8715'__34
v0
-- Declarative.conv⊢
d_conv'8866'_198 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  T_Ctx_16 ->
  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 ->
  T__'8866'__110 -> T__'8866'__110
d_conv'8866'_198 :: 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__'8866'__110
-> T__'8866'__110
d_conv'8866'_198 ~T_Ctx'8902'_2
v0 ~T_Ctx_16
v1 ~T_Ctx_16
v2 ~T__'8866''8902'__20
v3 ~T__'8866''8902'__20
v4 ~T__'8801'__12
v5 ~T__'8801'__12
v6 T__'8866'__110
v7
  = T__'8866'__110 -> T__'8866'__110
du_conv'8866'_198 T__'8866'__110
v7
du_conv'8866'_198 :: T__'8866'__110 -> T__'8866'__110
du_conv'8866'_198 :: T__'8866'__110 -> T__'8866'__110
du_conv'8866'_198 T__'8866'__110
v0 = T__'8866'__110 -> T__'8866'__110
forall a b. a -> b
coe T__'8866'__110
v0
-- Declarative.typeOf
d_typeOf_204 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  T_Ctx_16 -> T__'8866'__110 -> MAlonzo.Code.Type.T__'8866''8902'__20
d_typeOf_204 :: T_Ctx'8902'_2
-> T__'8866''8902'__20
-> T_Ctx_16
-> T__'8866'__110
-> T__'8866''8902'__20
d_typeOf_204 ~T_Ctx'8902'_2
v0 T__'8866''8902'__20
v1 ~T_Ctx_16
v2 ~T__'8866'__110
v3 = T__'8866''8902'__20 -> T__'8866''8902'__20
du_typeOf_204 T__'8866''8902'__20
v1
du_typeOf_204 ::
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  MAlonzo.Code.Type.T__'8866''8902'__20
du_typeOf_204 :: T__'8866''8902'__20 -> T__'8866''8902'__20
du_typeOf_204 T__'8866''8902'__20
v0 = T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8866''8902'__20
v0
-- Declarative.typeOf∋
d_typeOf'8715'_210 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  T_Ctx_16 -> T__'8715'__34 -> MAlonzo.Code.Type.T__'8866''8902'__20
d_typeOf'8715'_210 :: T_Ctx'8902'_2
-> T__'8866''8902'__20
-> T_Ctx_16
-> T__'8715'__34
-> T__'8866''8902'__20
d_typeOf'8715'_210 ~T_Ctx'8902'_2
v0 T__'8866''8902'__20
v1 ~T_Ctx_16
v2 ~T__'8715'__34
v3 = T__'8866''8902'__20 -> T__'8866''8902'__20
du_typeOf'8715'_210 T__'8866''8902'__20
v1
du_typeOf'8715'_210 ::
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  MAlonzo.Code.Type.T__'8866''8902'__20
du_typeOf'8715'_210 :: T__'8866''8902'__20 -> T__'8866''8902'__20
du_typeOf'8715'_210 T__'8866''8902'__20
v0 = T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8866''8902'__20
v0
-- Declarative.piBody
d_piBody_216 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  T_Ctx_16 ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  T__'8866'__110 -> MAlonzo.Code.Type.T__'8866''8902'__20
d_piBody_216 :: T_Ctx'8902'_2
-> T_Kind_476
-> T_Ctx_16
-> T__'8866''8902'__20
-> T__'8866'__110
-> T__'8866''8902'__20
d_piBody_216 ~T_Ctx'8902'_2
v0 ~T_Kind_476
v1 ~T_Ctx_16
v2 T__'8866''8902'__20
v3 ~T__'8866'__110
v4 = T__'8866''8902'__20 -> T__'8866''8902'__20
du_piBody_216 T__'8866''8902'__20
v3
du_piBody_216 ::
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  MAlonzo.Code.Type.T__'8866''8902'__20
du_piBody_216 :: T__'8866''8902'__20 -> T__'8866''8902'__20
du_piBody_216 T__'8866''8902'__20
v0 = T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8866''8902'__20
v0
-- Declarative.muPat
d_muPat_222 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  T_Ctx_16 ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  T__'8866'__110 -> MAlonzo.Code.Type.T__'8866''8902'__20
d_muPat_222 :: T_Ctx'8902'_2
-> T_Kind_476
-> T_Ctx_16
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866'__110
-> T__'8866''8902'__20
d_muPat_222 ~T_Ctx'8902'_2
v0 ~T_Kind_476
v1 ~T_Ctx_16
v2 ~T__'8866''8902'__20
v3 T__'8866''8902'__20
v4 ~T__'8866'__110
v5 = T__'8866''8902'__20 -> T__'8866''8902'__20
du_muPat_222 T__'8866''8902'__20
v4
du_muPat_222 ::
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  MAlonzo.Code.Type.T__'8866''8902'__20
du_muPat_222 :: T__'8866''8902'__20 -> T__'8866''8902'__20
du_muPat_222 T__'8866''8902'__20
v0 = T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8866''8902'__20
v0
-- Declarative.muArg
d_muArg_228 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  T_Ctx_16 ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  T__'8866'__110 -> MAlonzo.Code.Type.T__'8866''8902'__20
d_muArg_228 :: T_Ctx'8902'_2
-> T_Kind_476
-> T_Ctx_16
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866'__110
-> T__'8866''8902'__20
d_muArg_228 ~T_Ctx'8902'_2
v0 ~T_Kind_476
v1 ~T_Ctx_16
v2 ~T__'8866''8902'__20
v3 T__'8866''8902'__20
v4 ~T__'8866'__110
v5 = T__'8866''8902'__20 -> T__'8866''8902'__20
du_muArg_228 T__'8866''8902'__20
v4
du_muArg_228 ::
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  MAlonzo.Code.Type.T__'8866''8902'__20
du_muArg_228 :: T__'8866''8902'__20 -> T__'8866''8902'__20
du_muArg_228 T__'8866''8902'__20
v0 = T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8866''8902'__20
v0