{-# 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.Bool.Properties
import qualified MAlonzo.Code.Data.Char.Base
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.String
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)
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_32) -> Text -> [Text])
-> AgdaAny -> Text -> [Text]
forall a b. a -> b
coe
(T_Char_6 -> T_Dec_32) -> Text -> [Text]
MAlonzo.Code.Data.String.du_wordsBy_148
((AgdaAny -> T_Dec_32) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v0 ->
Bool -> T_Dec_32
MAlonzo.Code.Data.Bool.Properties.d_T'63'_2210
((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
'.'))))
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_494 ([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)
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))
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))
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))
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)
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))
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)
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'__60
(((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
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
46 :: Integer) (Integer
3261772278397201327 :: Integer)
String
"Relation.Nullary._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
3261772278397201327 :: Integer)
String
"Relation.Nullary.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'_298
((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
46 :: Integer) (Integer
3261772278397201327 :: Integer)
String
"Relation.Nullary._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
3261772278397201327 :: Integer)
String
"Relation.Nullary.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'_298
((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)))))
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_334 () () 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_404 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_400 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'__60
(((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))))
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_334 () () 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_404 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_400 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))))
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))))
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_334 () () 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_404 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_400 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))))
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
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_334 () () 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_404 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_400 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)))