{-# 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.Utils.Reflection 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.List
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Reflection
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Char.Base
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.String.Base
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core

-- Utils.Reflection.constructors
d_constructors_4 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Definition_280 -> [AgdaAny]
d_constructors_4 :: T_Definition_280 -> [AgdaAny]
d_constructors_4 T_Definition_280
v0
  = let v1 :: b
v1 = [AgdaAny] -> b
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16 in
    AgdaAny -> [AgdaAny]
forall a b. a -> b
coe
      (case T_Definition_280 -> T_Definition_280
forall a b. a -> b
coe T_Definition_280
v0 of
         MAlonzo.Code.Agda.Builtin.Reflection.C_data'45'type_290 Integer
v2 [AgdaAny]
v3
           -> [AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3
         T_Definition_280
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {b}. b
v1)
-- Utils.Reflection.names
d_names_10 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  [MAlonzo.Code.Agda.Builtin.String.T_String_6]
d_names_10 :: Text -> [Text]
d_names_10
  = ((T_Char_6 -> T_Dec_20) -> Text -> [Text])
-> AgdaAny -> Text -> [Text]
forall a b. a -> b
coe
      (T_Char_6 -> T_Dec_20) -> Text -> [Text]
MAlonzo.Code.Data.String.Base.du_wordsBy_106
      ((AgdaAny -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v0 ->
            Bool -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.d_T'63'_66
              ((T_Char_6 -> T_Char_6 -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe
                 T_Char_6 -> T_Char_6 -> Bool
MAlonzo.Code.Data.Char.Base.d__'8776''7495'__14 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0)
                 (T_Char_6 -> AgdaAny
forall a b. a -> b
coe T_Char_6
'.'))))
-- Utils.Reflection.lastName
d_lastName_14 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  [MAlonzo.Code.Agda.Builtin.String.T_String_6] ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_lastName_14 :: Text -> [Text] -> Text
d_lastName_14 Text
v0 [Text]
v1
  = let v2 :: t
v2 = ([AgdaAny] -> Maybe AgdaAny) -> AgdaAny -> t
forall a b. a -> b
coe [AgdaAny] -> Maybe AgdaAny
MAlonzo.Code.Data.List.Base.du_last_540 ([Text] -> AgdaAny
forall a b. a -> b
coe [Text]
v1) in
    AgdaAny -> Text
forall a b. a -> b
coe
      (case AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe AgdaAny
forall {b}. b
v2 of
         MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v3 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3
         Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> Text -> AgdaAny
forall a b. a -> b
coe Text
v0
         Maybe AgdaAny
_ -> AgdaAny
forall {b}. b
MAlonzo.RTE.mazUnreachableError)
-- Utils.Reflection.getLastName
d_getLastName_34 ::
  AgdaAny -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_getLastName_34 :: AgdaAny -> Text
d_getLastName_34 AgdaAny
v0
  = (Text -> [Text] -> Text) -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
      Text -> [Text] -> Text
d_lastName_14 (Text -> AgdaAny
forall a b. a -> b
coe (Text
"defconstructorname" :: Data.Text.Text))
      ((Text -> [Text]) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         Text -> [Text]
d_names_10
         ((QName -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe QName -> Text
MAlonzo.Code.Agda.Builtin.Reflection.d_primShowQName_12 AgdaAny
v0))
-- Utils.Reflection.mk-cls
d_mk'45'cls_38 ::
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Reflection.T_Clause_160
d_mk'45'cls_38 :: AgdaAny -> T_Clause_160
d_mk'45'cls_38 AgdaAny
v0
  = ([T_Σ_14] -> [T_Arg_88] -> T_Term_154 -> T_Clause_160)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Clause_160
forall a b. a -> b
coe
      [T_Σ_14] -> [T_Arg_88] -> T_Term_154 -> T_Clause_160
MAlonzo.Code.Agda.Builtin.Reflection.C_clause_272
      ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)
      ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
         ((T_ArgInfo_76 -> AgdaAny -> T_Arg_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_ArgInfo_76 -> AgdaAny -> T_Arg_88
MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98
            ((T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76
MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82
               (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50)
               ((T_Relevance_56 -> T_Quantity_62 -> T_Modality_68)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Relevance_56 -> T_Quantity_62 -> T_Modality_68
MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74
                  (T_Relevance_56 -> AgdaAny
forall a b. a -> b
coe T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58)
                  (T_Quantity_62 -> AgdaAny
forall a b. a -> b
coe T_Quantity_62
MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66)))
            ((AgdaAny -> [T_Arg_88] -> T_Pattern_158)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               AgdaAny -> [T_Arg_88] -> T_Pattern_158
MAlonzo.Code.Agda.Builtin.Reflection.C_con_244 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0)
               ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)))
         ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
            ((T_ArgInfo_76 -> AgdaAny -> T_Arg_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_ArgInfo_76 -> AgdaAny -> T_Arg_88
MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98
               ((T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76
MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82
                  (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50)
                  ((T_Relevance_56 -> T_Quantity_62 -> T_Modality_68)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Relevance_56 -> T_Quantity_62 -> T_Modality_68
MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74
                     (T_Relevance_56 -> AgdaAny
forall a b. a -> b
coe T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58)
                     (T_Quantity_62 -> AgdaAny
forall a b. a -> b
coe T_Quantity_62
MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66)))
               ((AgdaAny -> [T_Arg_88] -> T_Pattern_158)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  AgdaAny -> [T_Arg_88] -> T_Pattern_158
MAlonzo.Code.Agda.Builtin.Reflection.C_con_244 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0)
                  ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)))
            ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)))
      ((AgdaAny -> [T_Arg_88] -> T_Term_154)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> [T_Arg_88] -> T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_con_178
         (QName -> AgdaAny
forall a b. a -> b
coe
            (Integer -> Integer -> String -> Fixity -> QName
MAlonzo.RTE.QName
               (Integer
10 :: Integer) (Integer
4305008439024043551 :: Integer)
               String
"Agda.Builtin.Bool.Bool.true"
               (Assoc -> Precedence -> Fixity
MAlonzo.RTE.Fixity Assoc
MAlonzo.RTE.NonAssoc Precedence
MAlonzo.RTE.Unrelated)))
         ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16))
-- Utils.Reflection.wildcard
d_wildcard_42 :: MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88
d_wildcard_42 :: T_Arg_88
d_wildcard_42
  = (T_ArgInfo_76 -> AgdaAny -> T_Arg_88)
-> AgdaAny -> AgdaAny -> T_Arg_88
forall a b. a -> b
coe
      T_ArgInfo_76 -> AgdaAny -> T_Arg_88
MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98
      ((T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76
MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82
         (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50)
         ((T_Relevance_56 -> T_Quantity_62 -> T_Modality_68)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Relevance_56 -> T_Quantity_62 -> T_Modality_68
MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74
            (T_Relevance_56 -> AgdaAny
forall a b. a -> b
coe T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58)
            (T_Quantity_62 -> AgdaAny
forall a b. a -> b
coe T_Quantity_62
MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66)))
      ((T_Term_154 -> T_Pattern_158) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Term_154 -> T_Pattern_158
MAlonzo.Code.Agda.Builtin.Reflection.C_dot_248
         (T_Term_154 -> AgdaAny
forall a b. a -> b
coe T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_216))
-- Utils.Reflection.absurd-lam
d_absurd'45'lam_44 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154
d_absurd'45'lam_44 :: T_Term_154
d_absurd'45'lam_44
  = ([T_Clause_160] -> [T_Arg_88] -> T_Term_154)
-> AgdaAny -> AgdaAny -> T_Term_154
forall a b. a -> b
coe
      [T_Clause_160] -> [T_Arg_88] -> T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_pat'45'lam_196
      ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
         (([T_Σ_14] -> [T_Arg_88] -> T_Clause_160)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            [T_Σ_14] -> [T_Arg_88] -> T_Clause_160
MAlonzo.Code.Agda.Builtin.Reflection.C_absurd'45'clause_278
            ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
               ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                  (Text -> AgdaAny
forall a b. a -> b
coe (Text
"()" :: Data.Text.Text))
                  ((T_ArgInfo_76 -> AgdaAny -> T_Arg_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_ArgInfo_76 -> AgdaAny -> T_Arg_88
MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98
                     ((T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76
MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82
                        (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50)
                        ((T_Relevance_56 -> T_Quantity_62 -> T_Modality_68)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_Relevance_56 -> T_Quantity_62 -> T_Modality_68
MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74
                           (T_Relevance_56 -> AgdaAny
forall a b. a -> b
coe T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58)
                           (T_Quantity_62 -> AgdaAny
forall a b. a -> b
coe T_Quantity_62
MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66)))
                     (T_Term_154 -> AgdaAny
forall a b. a -> b
coe T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_216)))
               ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16))
            ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
               ((T_ArgInfo_76 -> AgdaAny -> T_Arg_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_ArgInfo_76 -> AgdaAny -> T_Arg_88
MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98
                  ((T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76
MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82
                     (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50)
                     ((T_Relevance_56 -> T_Quantity_62 -> T_Modality_68)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Relevance_56 -> T_Quantity_62 -> T_Modality_68
MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74
                        (T_Relevance_56 -> AgdaAny
forall a b. a -> b
coe T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58)
                        (T_Quantity_62 -> AgdaAny
forall a b. a -> b
coe T_Quantity_62
MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66)))
                  ((Integer -> T_Pattern_158) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     Integer -> T_Pattern_158
MAlonzo.Code.Agda.Builtin.Reflection.C_absurd_264
                     (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
0 :: Integer))))
               ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)))
         ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16))
      ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)
-- Utils.Reflection.default-cls
d_default'45'cls_46 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Clause_160
d_default'45'cls_46 :: T_Clause_160
d_default'45'cls_46
  = ([T_Σ_14] -> [T_Arg_88] -> T_Term_154 -> T_Clause_160)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Clause_160
forall a b. a -> b
coe
      [T_Σ_14] -> [T_Arg_88] -> T_Term_154 -> T_Clause_160
MAlonzo.Code.Agda.Builtin.Reflection.C_clause_272
      ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)
      ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_Arg_88 -> AgdaAny
forall a b. a -> b
coe T_Arg_88
d_wildcard_42)
         ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_Arg_88 -> AgdaAny
forall a b. a -> b
coe T_Arg_88
d_wildcard_42)
            ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)))
      ((AgdaAny -> [T_Arg_88] -> T_Term_154)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> [T_Arg_88] -> T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_con_178
         (QName -> AgdaAny
forall a b. a -> b
coe
            (Integer -> Integer -> String -> Fixity -> QName
MAlonzo.RTE.QName
               (Integer
8 :: Integer) (Integer
4305008439024043551 :: Integer)
               String
"Agda.Builtin.Bool.Bool.false"
               (Assoc -> Precedence -> Fixity
MAlonzo.RTE.Fixity Assoc
MAlonzo.RTE.NonAssoc Precedence
MAlonzo.RTE.Unrelated)))
         ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16))
-- Utils.Reflection.map2
d_map2_56 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () -> (AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny]
d_map2_56 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
d_map2_56 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 [AgdaAny]
v5 = (AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny]
du_map2_56 AgdaAny -> AgdaAny -> AgdaAny
v4 [AgdaAny]
v5
du_map2_56 ::
  (AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny]
du_map2_56 :: (AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny]
du_map2_56 AgdaAny -> AgdaAny -> AgdaAny
v0 [AgdaAny]
v1 = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny] -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny]
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> [AgdaAny] -> [AgdaAny]
du_map2''_70 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1)
-- Utils.Reflection._.map2'
d_map2''_70 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] -> [AgdaAny] -> [AgdaAny]
d_map2''_70 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
d_map2''_70 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny
v4 ~[AgdaAny]
v5 AgdaAny -> AgdaAny -> AgdaAny
v6 [AgdaAny]
v7 [AgdaAny]
v8
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> [AgdaAny] -> [AgdaAny]
du_map2''_70 AgdaAny -> AgdaAny -> AgdaAny
v6 [AgdaAny]
v7 [AgdaAny]
v8
du_map2''_70 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] -> [AgdaAny] -> [AgdaAny]
du_map2''_70 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> [AgdaAny] -> [AgdaAny]
du_map2''_70 AgdaAny -> AgdaAny -> AgdaAny
v0 [AgdaAny]
v1 [AgdaAny]
v2
  = case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
      [] -> [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1
      (:) AgdaAny
v3 [AgdaAny]
v4
        -> ([AgdaAny] -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> [AgdaAny]
forall a b. a -> b
coe
             [AgdaAny] -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du__'43''43'__32
             (((AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_map_22 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2))
             (((AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny] -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> [AgdaAny] -> [AgdaAny]
du_map2''_70 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v4) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2))
      [AgdaAny]
_ -> [AgdaAny]
forall {b}. b
MAlonzo.RTE.mazUnreachableError
-- Utils.Reflection.mk-DecCls
d_mk'45'DecCls_82 ::
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Reflection.T_Clause_160
d_mk'45'DecCls_82 :: AgdaAny -> AgdaAny -> T_Clause_160
d_mk'45'DecCls_82 AgdaAny
v0 AgdaAny
v1
  = let v2 :: t
v2
          = (QName -> QName -> Bool) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
              QName -> QName -> Bool
MAlonzo.Code.Agda.Builtin.Reflection.d_primQNameEquality_8 AgdaAny
v0 AgdaAny
v1 in
    AgdaAny -> T_Clause_160
forall a b. a -> b
coe
      (if AgdaAny -> Bool
forall a b. a -> b
coe AgdaAny
forall {b}. b
v2
         then ([T_Σ_14] -> [T_Arg_88] -> T_Term_154 -> T_Clause_160)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                [T_Σ_14] -> [T_Arg_88] -> T_Term_154 -> T_Clause_160
MAlonzo.Code.Agda.Builtin.Reflection.C_clause_272
                ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)
                ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                   ((T_ArgInfo_76 -> AgdaAny -> T_Arg_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      T_ArgInfo_76 -> AgdaAny -> T_Arg_88
MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98
                      ((T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76
MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82
                         (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50)
                         ((T_Relevance_56 -> T_Quantity_62 -> T_Modality_68)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            T_Relevance_56 -> T_Quantity_62 -> T_Modality_68
MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74
                            (T_Relevance_56 -> AgdaAny
forall a b. a -> b
coe T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58)
                            (T_Quantity_62 -> AgdaAny
forall a b. a -> b
coe T_Quantity_62
MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66)))
                      ((AgdaAny -> [T_Arg_88] -> T_Pattern_158)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         AgdaAny -> [T_Arg_88] -> T_Pattern_158
MAlonzo.Code.Agda.Builtin.Reflection.C_con_244 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0)
                         ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)))
                   ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                      ((T_ArgInfo_76 -> AgdaAny -> T_Arg_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         T_ArgInfo_76 -> AgdaAny -> T_Arg_88
MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98
                         ((T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76
MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82
                            (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50)
                            ((T_Relevance_56 -> T_Quantity_62 -> T_Modality_68)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                               T_Relevance_56 -> T_Quantity_62 -> T_Modality_68
MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74
                               (T_Relevance_56 -> AgdaAny
forall a b. a -> b
coe T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58)
                               (T_Quantity_62 -> AgdaAny
forall a b. a -> b
coe T_Quantity_62
MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66)))
                         ((AgdaAny -> [T_Arg_88] -> T_Pattern_158)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            AgdaAny -> [T_Arg_88] -> T_Pattern_158
MAlonzo.Code.Agda.Builtin.Reflection.C_con_244 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
                            ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)))
                      ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)))
                ((AgdaAny -> [T_Arg_88] -> T_Term_154)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   AgdaAny -> [T_Arg_88] -> T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_con_178
                   (QName -> AgdaAny
forall a b. a -> b
coe
                      (Integer -> Integer -> String -> Fixity -> QName
MAlonzo.RTE.QName
                         (Integer
32 :: Integer) (Integer
16368259409245829246 :: Integer)
                         String
"Relation.Nullary.Decidable.Core._because_"
                         (Assoc -> Precedence -> Fixity
MAlonzo.RTE.Fixity
                            Assoc
MAlonzo.RTE.NonAssoc (PrecedenceLevel -> Precedence
MAlonzo.RTE.Related (PrecedenceLevel
2.0 :: Double)))))
                   ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                      ((T_ArgInfo_76 -> AgdaAny -> T_Arg_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         T_ArgInfo_76 -> AgdaAny -> T_Arg_88
MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98
                         ((T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76
MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82
                            (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50)
                            ((T_Relevance_56 -> T_Quantity_62 -> T_Modality_68)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                               T_Relevance_56 -> T_Quantity_62 -> T_Modality_68
MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74
                               (T_Relevance_56 -> AgdaAny
forall a b. a -> b
coe T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58)
                               (T_Quantity_62 -> AgdaAny
forall a b. a -> b
coe T_Quantity_62
MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66)))
                         ((AgdaAny -> [T_Arg_88] -> T_Term_154)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            AgdaAny -> [T_Arg_88] -> T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_con_178
                            (QName -> AgdaAny
forall a b. a -> b
coe
                               (Integer -> Integer -> String -> Fixity -> QName
MAlonzo.RTE.QName
                                  (Integer
10 :: Integer) (Integer
4305008439024043551 :: Integer)
                                  String
"Agda.Builtin.Bool.Bool.true"
                                  (Assoc -> Precedence -> Fixity
MAlonzo.RTE.Fixity Assoc
MAlonzo.RTE.NonAssoc Precedence
MAlonzo.RTE.Unrelated)))
                            ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)))
                      ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                         ((T_ArgInfo_76 -> AgdaAny -> T_Arg_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            T_ArgInfo_76 -> AgdaAny -> T_Arg_88
MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98
                            ((T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                               T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76
MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82
                               (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50)
                               ((T_Relevance_56 -> T_Quantity_62 -> T_Modality_68)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                  T_Relevance_56 -> T_Quantity_62 -> T_Modality_68
MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74
                                  (T_Relevance_56 -> AgdaAny
forall a b. a -> b
coe T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58)
                                  (T_Quantity_62 -> AgdaAny
forall a b. a -> b
coe T_Quantity_62
MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66)))
                            ((AgdaAny -> [T_Arg_88] -> T_Term_154)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                               AgdaAny -> [T_Arg_88] -> T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_con_178
                               (QName -> AgdaAny
forall a b. a -> b
coe
                                  (Integer -> Integer -> String -> Fixity -> QName
MAlonzo.RTE.QName
                                     (Integer
22 :: Integer) (Integer
5284306542668000596 :: Integer)
                                     String
"Relation.Nullary.Reflects.Reflects.of\696"
                                     (Assoc -> Precedence -> Fixity
MAlonzo.RTE.Fixity
                                        Assoc
MAlonzo.RTE.NonAssoc Precedence
MAlonzo.RTE.Unrelated)))
                               ((AgdaAny -> [AgdaAny]) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                  AgdaAny -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_'91'_'93'_286
                                  ((T_ArgInfo_76 -> AgdaAny -> T_Arg_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     T_ArgInfo_76 -> AgdaAny -> T_Arg_88
MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98
                                     ((T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76
MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82
                                        (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50)
                                        ((T_Relevance_56 -> T_Quantity_62 -> T_Modality_68)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           T_Relevance_56 -> T_Quantity_62 -> T_Modality_68
MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74
                                           (T_Relevance_56 -> AgdaAny
forall a b. a -> b
coe T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58)
                                           (T_Quantity_62 -> AgdaAny
forall a b. a -> b
coe
                                              T_Quantity_62
MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66)))
                                     ((AgdaAny -> [T_Arg_88] -> T_Term_154)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> [T_Arg_88] -> T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_con_178
                                        (QName -> AgdaAny
forall a b. a -> b
coe
                                           (Integer -> Integer -> String -> Fixity -> QName
MAlonzo.RTE.QName
                                              (Integer
20 :: Integer) (Integer
1335258922519917603 :: Integer)
                                              String
"Agda.Builtin.Equality._\8801_.refl"
                                              (Assoc -> Precedence -> Fixity
MAlonzo.RTE.Fixity
                                                 Assoc
MAlonzo.RTE.NonAssoc Precedence
MAlonzo.RTE.Unrelated)))
                                        ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16))))))
                         ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16))))
         else ([T_Σ_14] -> [T_Arg_88] -> T_Term_154 -> T_Clause_160)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                [T_Σ_14] -> [T_Arg_88] -> T_Term_154 -> T_Clause_160
MAlonzo.Code.Agda.Builtin.Reflection.C_clause_272
                ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)
                ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                   ((T_ArgInfo_76 -> AgdaAny -> T_Arg_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      T_ArgInfo_76 -> AgdaAny -> T_Arg_88
MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98
                      ((T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76
MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82
                         (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50)
                         ((T_Relevance_56 -> T_Quantity_62 -> T_Modality_68)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            T_Relevance_56 -> T_Quantity_62 -> T_Modality_68
MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74
                            (T_Relevance_56 -> AgdaAny
forall a b. a -> b
coe T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58)
                            (T_Quantity_62 -> AgdaAny
forall a b. a -> b
coe T_Quantity_62
MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66)))
                      ((AgdaAny -> [T_Arg_88] -> T_Pattern_158)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         AgdaAny -> [T_Arg_88] -> T_Pattern_158
MAlonzo.Code.Agda.Builtin.Reflection.C_con_244 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0)
                         ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)))
                   ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                      ((T_ArgInfo_76 -> AgdaAny -> T_Arg_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         T_ArgInfo_76 -> AgdaAny -> T_Arg_88
MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98
                         ((T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76
MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82
                            (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50)
                            ((T_Relevance_56 -> T_Quantity_62 -> T_Modality_68)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                               T_Relevance_56 -> T_Quantity_62 -> T_Modality_68
MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74
                               (T_Relevance_56 -> AgdaAny
forall a b. a -> b
coe T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58)
                               (T_Quantity_62 -> AgdaAny
forall a b. a -> b
coe T_Quantity_62
MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66)))
                         ((AgdaAny -> [T_Arg_88] -> T_Pattern_158)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            AgdaAny -> [T_Arg_88] -> T_Pattern_158
MAlonzo.Code.Agda.Builtin.Reflection.C_con_244 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
                            ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)))
                      ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)))
                ((AgdaAny -> [T_Arg_88] -> T_Term_154)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   AgdaAny -> [T_Arg_88] -> T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_con_178
                   (QName -> AgdaAny
forall a b. a -> b
coe
                      (Integer -> Integer -> String -> Fixity -> QName
MAlonzo.RTE.QName
                         (Integer
32 :: Integer) (Integer
16368259409245829246 :: Integer)
                         String
"Relation.Nullary.Decidable.Core._because_"
                         (Assoc -> Precedence -> Fixity
MAlonzo.RTE.Fixity
                            Assoc
MAlonzo.RTE.NonAssoc (PrecedenceLevel -> Precedence
MAlonzo.RTE.Related (PrecedenceLevel
2.0 :: Double)))))
                   ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                      ((T_ArgInfo_76 -> AgdaAny -> T_Arg_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         T_ArgInfo_76 -> AgdaAny -> T_Arg_88
MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98
                         ((T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76
MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82
                            (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50)
                            ((T_Relevance_56 -> T_Quantity_62 -> T_Modality_68)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                               T_Relevance_56 -> T_Quantity_62 -> T_Modality_68
MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74
                               (T_Relevance_56 -> AgdaAny
forall a b. a -> b
coe T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58)
                               (T_Quantity_62 -> AgdaAny
forall a b. a -> b
coe T_Quantity_62
MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66)))
                         ((AgdaAny -> [T_Arg_88] -> T_Term_154)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            AgdaAny -> [T_Arg_88] -> T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_con_178
                            (QName -> AgdaAny
forall a b. a -> b
coe
                               (Integer -> Integer -> String -> Fixity -> QName
MAlonzo.RTE.QName
                                  (Integer
8 :: Integer) (Integer
4305008439024043551 :: Integer)
                                  String
"Agda.Builtin.Bool.Bool.false"
                                  (Assoc -> Precedence -> Fixity
MAlonzo.RTE.Fixity Assoc
MAlonzo.RTE.NonAssoc Precedence
MAlonzo.RTE.Unrelated)))
                            ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)))
                      ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                         ((T_ArgInfo_76 -> AgdaAny -> T_Arg_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            T_ArgInfo_76 -> AgdaAny -> T_Arg_88
MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98
                            ((T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                               T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76
MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82
                               (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50)
                               ((T_Relevance_56 -> T_Quantity_62 -> T_Modality_68)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                  T_Relevance_56 -> T_Quantity_62 -> T_Modality_68
MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74
                                  (T_Relevance_56 -> AgdaAny
forall a b. a -> b
coe T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58)
                                  (T_Quantity_62 -> AgdaAny
forall a b. a -> b
coe T_Quantity_62
MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66)))
                            ((AgdaAny -> [T_Arg_88] -> T_Term_154)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                               AgdaAny -> [T_Arg_88] -> T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_con_178
                               (QName -> AgdaAny
forall a b. a -> b
coe
                                  (Integer -> Integer -> String -> Fixity -> QName
MAlonzo.RTE.QName
                                     (Integer
26 :: Integer) (Integer
5284306542668000596 :: Integer)
                                     String
"Relation.Nullary.Reflects.Reflects.of\8319"
                                     (Assoc -> Precedence -> Fixity
MAlonzo.RTE.Fixity
                                        Assoc
MAlonzo.RTE.NonAssoc Precedence
MAlonzo.RTE.Unrelated)))
                               ((AgdaAny -> [AgdaAny]) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                  AgdaAny -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_'91'_'93'_286
                                  ((T_ArgInfo_76 -> AgdaAny -> T_Arg_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     T_ArgInfo_76 -> AgdaAny -> T_Arg_88
MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98
                                     ((T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76
MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82
                                        (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50)
                                        ((T_Relevance_56 -> T_Quantity_62 -> T_Modality_68)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           T_Relevance_56 -> T_Quantity_62 -> T_Modality_68
MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74
                                           (T_Relevance_56 -> AgdaAny
forall a b. a -> b
coe T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58)
                                           (T_Quantity_62 -> AgdaAny
forall a b. a -> b
coe
                                              T_Quantity_62
MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66)))
                                     (T_Term_154 -> AgdaAny
forall a b. a -> b
coe T_Term_154
d_absurd'45'lam_44)))))
                         ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)))))
-- Utils.Reflection.defEq
d_defEq_100 :: AgdaAny -> AgdaAny -> AgdaAny
d_defEq_100 :: AgdaAny -> AgdaAny -> AgdaAny
d_defEq_100 AgdaAny
v0 AgdaAny
v1
  = AgdaAny
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
      AgdaAny
forall {b}. b
MAlonzo.Code.Agda.Builtin.Reflection.d_bindTC_336 () () AgdaAny
forall {b}. b
erased
      AgdaAny
forall {b}. b
erased
      (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {b}. b
MAlonzo.Code.Agda.Builtin.Reflection.d_getDefinition_408 AgdaAny
v0)
      (\ AgdaAny
v2 ->
         AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           AgdaAny
forall {b}. b
MAlonzo.Code.Agda.Builtin.Reflection.d_defineFun_404 AgdaAny
v1
           (([AgdaAny] -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              [AgdaAny] -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du__'43''43'__32
              (((AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 (AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_map_22 ((AgdaAny -> T_Clause_160) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Clause_160
d_mk'45'cls_38)
                 ((T_Definition_280 -> [AgdaAny]) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Definition_280 -> [AgdaAny]
d_constructors_4 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)))
              ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                 (T_Clause_160 -> AgdaAny
forall a b. a -> b
coe T_Clause_160
d_default'45'cls_46)
                 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16))))
-- Utils.Reflection.defDec
d_defDec_110 :: AgdaAny -> AgdaAny -> AgdaAny
d_defDec_110 :: AgdaAny -> AgdaAny -> AgdaAny
d_defDec_110 AgdaAny
v0 AgdaAny
v1
  = AgdaAny
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
      AgdaAny
forall {b}. b
MAlonzo.Code.Agda.Builtin.Reflection.d_bindTC_336 () () AgdaAny
forall {b}. b
erased
      AgdaAny
forall {b}. b
erased
      (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {b}. b
MAlonzo.Code.Agda.Builtin.Reflection.d_getDefinition_408 AgdaAny
v0)
      (\ AgdaAny
v2 ->
         AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           AgdaAny
forall {b}. b
MAlonzo.Code.Agda.Builtin.Reflection.d_defineFun_404 AgdaAny
v1
           (((AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              (AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny]
du_map2_56 ((AgdaAny -> AgdaAny -> T_Clause_160) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Clause_160
d_mk'45'DecCls_82)
              ((T_Definition_280 -> [AgdaAny]) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Definition_280 -> [AgdaAny]
d_constructors_4 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))))
-- Utils.Reflection.mk-Show
d_mk'45'Show_120 ::
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Reflection.T_Clause_160
d_mk'45'Show_120 :: AgdaAny -> T_Clause_160
d_mk'45'Show_120 AgdaAny
v0
  = ([T_Σ_14] -> [T_Arg_88] -> T_Term_154 -> T_Clause_160)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Clause_160
forall a b. a -> b
coe
      [T_Σ_14] -> [T_Arg_88] -> T_Term_154 -> T_Clause_160
MAlonzo.Code.Agda.Builtin.Reflection.C_clause_272
      ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)
      ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
         ((T_ArgInfo_76 -> AgdaAny -> T_Arg_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_ArgInfo_76 -> AgdaAny -> T_Arg_88
MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98
            ((T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76
MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82
               (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50)
               ((T_Relevance_56 -> T_Quantity_62 -> T_Modality_68)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Relevance_56 -> T_Quantity_62 -> T_Modality_68
MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74
                  (T_Relevance_56 -> AgdaAny
forall a b. a -> b
coe T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58)
                  (T_Quantity_62 -> AgdaAny
forall a b. a -> b
coe T_Quantity_62
MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66)))
            ((AgdaAny -> [T_Arg_88] -> T_Pattern_158)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               AgdaAny -> [T_Arg_88] -> T_Pattern_158
MAlonzo.Code.Agda.Builtin.Reflection.C_con_244 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0)
               ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)))
         ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16))
      ((T_Literal_124 -> T_Term_154) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Literal_124 -> T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_lit_210
         ((Text -> T_Literal_124) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            Text -> T_Literal_124
MAlonzo.Code.Agda.Builtin.Reflection.C_string_144
            ((AgdaAny -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Text
d_getLastName_34 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0))))
-- Utils.Reflection.defShow
d_defShow_124 :: AgdaAny -> AgdaAny -> AgdaAny
d_defShow_124 :: AgdaAny -> AgdaAny -> AgdaAny
d_defShow_124 AgdaAny
v0 AgdaAny
v1
  = AgdaAny
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
      AgdaAny
forall {b}. b
MAlonzo.Code.Agda.Builtin.Reflection.d_bindTC_336 () () AgdaAny
forall {b}. b
erased
      AgdaAny
forall {b}. b
erased
      (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {b}. b
MAlonzo.Code.Agda.Builtin.Reflection.d_getDefinition_408 AgdaAny
v0)
      (\ AgdaAny
v2 ->
         AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           AgdaAny
forall {b}. b
MAlonzo.Code.Agda.Builtin.Reflection.d_defineFun_404 AgdaAny
v1
           (((AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              (AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_map_22 ((AgdaAny -> T_Clause_160) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Clause_160
d_mk'45'Show_120)
              ((T_Definition_280 -> [AgdaAny]) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Definition_280 -> [AgdaAny]
d_constructors_4 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))))
-- Utils.Reflection.mkList
d_mkList_134 ::
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154] ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154
d_mkList_134 :: [T_Term_154] -> T_Term_154
d_mkList_134 [T_Term_154]
v0
  = case [T_Term_154] -> [AgdaAny]
forall a b. a -> b
coe [T_Term_154]
v0 of
      []
        -> (AgdaAny -> [T_Arg_88] -> T_Term_154)
-> AgdaAny -> AgdaAny -> T_Term_154
forall a b. a -> b
coe
             AgdaAny -> [T_Arg_88] -> T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_con_178
             (QName -> AgdaAny
forall a b. a -> b
coe
                (Integer -> Integer -> String -> Fixity -> QName
MAlonzo.RTE.QName
                   (Integer
16 :: Integer) (Integer
15090436609435731260 :: Integer)
                   String
"Agda.Builtin.List.List.[]"
                   (Assoc -> Precedence -> Fixity
MAlonzo.RTE.Fixity Assoc
MAlonzo.RTE.NonAssoc Precedence
MAlonzo.RTE.Unrelated)))
             ([T_Term_154] -> AgdaAny
forall a b. a -> b
coe [T_Term_154]
v0)
      (:) AgdaAny
v1 [AgdaAny]
v2
        -> (AgdaAny -> [T_Arg_88] -> T_Term_154)
-> AgdaAny -> AgdaAny -> T_Term_154
forall a b. a -> b
coe
             AgdaAny -> [T_Arg_88] -> T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_con_178
             (QName -> AgdaAny
forall a b. a -> b
coe
                (Integer -> Integer -> String -> Fixity -> QName
MAlonzo.RTE.QName
                   (Integer
22 :: Integer) (Integer
15090436609435731260 :: Integer)
                   String
"Agda.Builtin.List.List._\8759_"
                   (Assoc -> Precedence -> Fixity
MAlonzo.RTE.Fixity
                      Assoc
MAlonzo.RTE.RightAssoc (PrecedenceLevel -> Precedence
MAlonzo.RTE.Related (PrecedenceLevel
5.0 :: Double)))))
             ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                ((T_ArgInfo_76 -> AgdaAny -> T_Arg_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   T_ArgInfo_76 -> AgdaAny -> T_Arg_88
MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98
                   ((T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76
MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82
                      (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_hidden_52)
                      ((T_Relevance_56 -> T_Quantity_62 -> T_Modality_68)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         T_Relevance_56 -> T_Quantity_62 -> T_Modality_68
MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74
                         (T_Relevance_56 -> AgdaAny
forall a b. a -> b
coe T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58)
                         (T_Quantity_62 -> AgdaAny
forall a b. a -> b
coe T_Quantity_62
MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66)))
                   (T_Term_154 -> AgdaAny
forall a b. a -> b
coe T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_216))
                ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                   ((T_ArgInfo_76 -> AgdaAny -> T_Arg_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      T_ArgInfo_76 -> AgdaAny -> T_Arg_88
MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98
                      ((T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76
MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82
                         (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_hidden_52)
                         ((T_Relevance_56 -> T_Quantity_62 -> T_Modality_68)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            T_Relevance_56 -> T_Quantity_62 -> T_Modality_68
MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74
                            (T_Relevance_56 -> AgdaAny
forall a b. a -> b
coe T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58)
                            (T_Quantity_62 -> AgdaAny
forall a b. a -> b
coe T_Quantity_62
MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66)))
                      (T_Term_154 -> AgdaAny
forall a b. a -> b
coe T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_216))
                   ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                      ((T_ArgInfo_76 -> AgdaAny -> T_Arg_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         T_ArgInfo_76 -> AgdaAny -> T_Arg_88
MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98
                         ((T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76
MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82
                            (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50)
                            ((T_Relevance_56 -> T_Quantity_62 -> T_Modality_68)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                               T_Relevance_56 -> T_Quantity_62 -> T_Modality_68
MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74
                               (T_Relevance_56 -> AgdaAny
forall a b. a -> b
coe T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58)
                               (T_Quantity_62 -> AgdaAny
forall a b. a -> b
coe T_Quantity_62
MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66)))
                         (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
                      ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                         ((T_ArgInfo_76 -> AgdaAny -> T_Arg_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            T_ArgInfo_76 -> AgdaAny -> T_Arg_88
MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98
                            ((T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                               T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76
MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82
                               (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50)
                               ((T_Relevance_56 -> T_Quantity_62 -> T_Modality_68)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                  T_Relevance_56 -> T_Quantity_62 -> T_Modality_68
MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74
                                  (T_Relevance_56 -> AgdaAny
forall a b. a -> b
coe T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58)
                                  (T_Quantity_62 -> AgdaAny
forall a b. a -> b
coe T_Quantity_62
MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66)))
                            (([T_Term_154] -> T_Term_154) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Term_154] -> T_Term_154
d_mkList_134 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2)))
                         ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)))))
      [AgdaAny]
_ -> T_Term_154
forall {b}. b
MAlonzo.RTE.mazUnreachableError
-- Utils.Reflection.defListConstructors
d_defListConstructors_140 :: AgdaAny -> AgdaAny -> AgdaAny
d_defListConstructors_140 :: AgdaAny -> AgdaAny -> AgdaAny
d_defListConstructors_140 AgdaAny
v0 AgdaAny
v1
  = AgdaAny
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
      AgdaAny
forall {b}. b
MAlonzo.Code.Agda.Builtin.Reflection.d_bindTC_336 () () AgdaAny
forall {b}. b
erased
      AgdaAny
forall {b}. b
erased
      (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {b}. b
MAlonzo.Code.Agda.Builtin.Reflection.d_getDefinition_408 AgdaAny
v0)
      (\ AgdaAny
v2 ->
         AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           AgdaAny
forall {b}. b
MAlonzo.Code.Agda.Builtin.Reflection.d_defineFun_404 AgdaAny
v1
           ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
              (([T_Σ_14] -> [T_Arg_88] -> T_Term_154 -> T_Clause_160)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 [T_Σ_14] -> [T_Arg_88] -> T_Term_154 -> T_Clause_160
MAlonzo.Code.Agda.Builtin.Reflection.C_clause_272
                 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)
                 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)
                 (([T_Term_154] -> T_Term_154) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    [T_Term_154] -> T_Term_154
d_mkList_134
                    (((AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       (AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_map_22
                       ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                          (\ AgdaAny
v3 ->
                             (AgdaAny -> [T_Arg_88] -> T_Term_154)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                               AgdaAny -> [T_Arg_88] -> T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_con_178 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
                               ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)))
                       ((T_Definition_280 -> [AgdaAny]) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Definition_280 -> [AgdaAny]
d_constructors_4 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)))))
              ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)))