{-# 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.Agda.Builtin.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.Bool
import qualified MAlonzo.Code.Agda.Builtin.Char
import qualified MAlonzo.Code.Agda.Builtin.Float
import qualified MAlonzo.Code.Agda.Builtin.List
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Agda.Primitive

-- Agda.Builtin.Reflection.Name
d_Name_6 :: a
d_Name_6
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Agda.Builtin.Reflection.Name"
-- Agda.Builtin.Reflection.primQNameEquality
d_primQNameEquality_8 :: QName -> QName -> Bool
d_primQNameEquality_8
  = (\ QName
x QName
y -> (QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
(==) :: MAlonzo.RTE.QName -> MAlonzo.RTE.QName -> Bool) ( QName
x) ( QName
y))
-- Agda.Builtin.Reflection.primQNameLess
d_primQNameLess_10 :: QName -> QName -> Bool
d_primQNameLess_10
  = (\ QName
x QName
y -> (QName -> QName -> Bool
forall a. Ord a => a -> a -> Bool
(<) :: MAlonzo.RTE.QName -> MAlonzo.RTE.QName -> Bool) ( QName
x) ( QName
y))
-- Agda.Builtin.Reflection.primShowQName
d_primShowQName_12 :: QName -> Text
d_primShowQName_12 = [Char] -> Text
Data.Text.pack ([Char] -> Text) -> (QName -> [Char]) -> QName -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> [Char]
MAlonzo.RTE.qnameString
-- Agda.Builtin.Reflection.Associativity
d_Associativity_14 :: ()
d_Associativity_14 = ()
type T_Associativity_14 = MAlonzo.RTE.Assoc
pattern $mC_left'45'assoc_16 :: forall {r}. Assoc -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_left'45'assoc_16 :: Assoc
C_left'45'assoc_16 = MAlonzo.RTE.LeftAssoc
pattern $mC_right'45'assoc_18 :: forall {r}. Assoc -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_right'45'assoc_18 :: Assoc
C_right'45'assoc_18 = MAlonzo.RTE.RightAssoc
pattern $mC_non'45'assoc_20 :: forall {r}. Assoc -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_non'45'assoc_20 :: Assoc
C_non'45'assoc_20 = MAlonzo.RTE.NonAssoc
check_left'45'assoc_16 :: T_Associativity_14
check_left'45'assoc_16 :: Assoc
check_left'45'assoc_16 = Assoc
MAlonzo.RTE.LeftAssoc
check_right'45'assoc_18 :: T_Associativity_14
check_right'45'assoc_18 :: Assoc
check_right'45'assoc_18 = Assoc
MAlonzo.RTE.RightAssoc
check_non'45'assoc_20 :: T_Associativity_14
check_non'45'assoc_20 :: Assoc
check_non'45'assoc_20 = Assoc
MAlonzo.RTE.NonAssoc
cover_Associativity_14 :: MAlonzo.RTE.Assoc -> ()
cover_Associativity_14 :: Assoc -> ()
cover_Associativity_14 Assoc
x
  = case Assoc
x of
      Assoc
MAlonzo.RTE.LeftAssoc -> ()
      Assoc
MAlonzo.RTE.RightAssoc -> ()
      Assoc
MAlonzo.RTE.NonAssoc -> ()
-- Agda.Builtin.Reflection.Precedence
d_Precedence_22 :: ()
d_Precedence_22 = ()
type T_Precedence_22 = MAlonzo.RTE.Precedence
pattern $mC_related_24 :: forall {r}.
Precedence -> (PrecedenceLevel -> r) -> ((# #) -> r) -> r
$bC_related_24 :: PrecedenceLevel -> Precedence
C_related_24 a0 = MAlonzo.RTE.Related a0
pattern $mC_unrelated_26 :: forall {r}. Precedence -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_unrelated_26 :: Precedence
C_unrelated_26 = MAlonzo.RTE.Unrelated
check_related_24 ::
  MAlonzo.Code.Agda.Builtin.Float.T_Float_6 -> T_Precedence_22
check_related_24 :: PrecedenceLevel -> Precedence
check_related_24 = PrecedenceLevel -> Precedence
MAlonzo.RTE.Related
check_unrelated_26 :: T_Precedence_22
check_unrelated_26 :: Precedence
check_unrelated_26 = Precedence
MAlonzo.RTE.Unrelated
cover_Precedence_22 :: MAlonzo.RTE.Precedence -> ()
cover_Precedence_22 :: Precedence -> ()
cover_Precedence_22 Precedence
x
  = case Precedence
x of
      MAlonzo.RTE.Related PrecedenceLevel
_ -> ()
      Precedence
MAlonzo.RTE.Unrelated -> ()
-- Agda.Builtin.Reflection.Fixity
d_Fixity_28 :: ()
d_Fixity_28 = ()
type T_Fixity_28 = MAlonzo.RTE.Fixity
pattern $mC_fixity_30 :: forall {r}.
Fixity -> (Assoc -> Precedence -> r) -> ((# #) -> r) -> r
$bC_fixity_30 :: Assoc -> Precedence -> Fixity
C_fixity_30 a0 a1 = MAlonzo.RTE.Fixity a0 a1
check_fixity_30 ::
  T_Associativity_14 -> T_Precedence_22 -> T_Fixity_28
check_fixity_30 :: Assoc -> Precedence -> Fixity
check_fixity_30 = Assoc -> Precedence -> Fixity
MAlonzo.RTE.Fixity
cover_Fixity_28 :: MAlonzo.RTE.Fixity -> ()
cover_Fixity_28 :: Fixity -> ()
cover_Fixity_28 Fixity
x
  = case Fixity
x of
      MAlonzo.RTE.Fixity Assoc
_ Precedence
_ -> ()
-- Agda.Builtin.Reflection.primQNameFixity
d_primQNameFixity_32 :: QName -> Fixity
d_primQNameFixity_32 = QName -> Fixity
MAlonzo.RTE.qnameFixity
-- Agda.Builtin.Reflection.primQNameToWord64s
d_primQNameToWord64s_36 :: QName -> (Integer, Integer)
d_primQNameToWord64s_36
  = \ QName
qn -> (QName -> Integer
MAlonzo.RTE.nameId QName
qn, QName -> Integer
MAlonzo.RTE.moduleId QName
qn)
-- Agda.Builtin.Reflection.Meta
d_Meta_38 :: a
d_Meta_38
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Agda.Builtin.Reflection.Meta"
-- Agda.Builtin.Reflection.primMetaEquality
d_primMetaEquality_40 :: (Integer, Integer) -> (Integer, Integer) -> Bool
d_primMetaEquality_40
  = (\ (Integer, Integer)
x (Integer, Integer)
y -> ((Integer, Integer) -> (Integer, Integer) -> Bool
forall a. Eq a => a -> a -> Bool
(==) :: (Integer, Integer) -> (Integer, Integer) -> Bool) ( (Integer, Integer)
x) ( (Integer, Integer)
y))
-- Agda.Builtin.Reflection.primMetaLess
d_primMetaLess_42 :: (Integer, Integer) -> (Integer, Integer) -> Bool
d_primMetaLess_42
  = (\ (Integer, Integer)
x (Integer, Integer)
y -> ((Integer, Integer) -> (Integer, Integer) -> Bool
forall a. Ord a => a -> a -> Bool
(<) :: (Integer, Integer) -> (Integer, Integer) -> Bool) ( (Integer, Integer)
x) ( (Integer, Integer)
y))
-- Agda.Builtin.Reflection.primShowMeta
d_primShowMeta_44 :: (Integer, Integer) -> Text
d_primShowMeta_44
  = \ (Integer
m, Integer
h) -> [Char] -> Text
Data.Text.pack ([Char]
"_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show (Integer
m :: Integer) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"@" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show (Integer
h :: Integer))
-- Agda.Builtin.Reflection.primMetaToNat
d_primMetaToNat_46 :: (Integer, Integer) -> Integer
d_primMetaToNat_46
  = \ (Integer
m, Integer
h) -> (Integer
h :: Integer) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
2Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
64 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ (Integer
m :: Integer)
-- Agda.Builtin.Reflection.Visibility
d_Visibility_48 :: ()
d_Visibility_48 = ()
data T_Visibility_48
  = C_visible_50 | C_hidden_52 | C_instance'8242'_54
-- Agda.Builtin.Reflection.Relevance
d_Relevance_56 :: ()
d_Relevance_56 = ()
data T_Relevance_56 = C_relevant_58 | C_irrelevant_60
-- Agda.Builtin.Reflection.Quantity
d_Quantity_62 :: ()
d_Quantity_62 = ()
data T_Quantity_62 = C_quantity'45'0_64 | C_quantity'45'ω_66
-- Agda.Builtin.Reflection.Modality
d_Modality_68 :: ()
d_Modality_68 = ()
data T_Modality_68 = C_modality_74 T_Relevance_56 T_Quantity_62
-- Agda.Builtin.Reflection.ArgInfo
d_ArgInfo_76 :: ()
d_ArgInfo_76 = ()
data T_ArgInfo_76 = C_arg'45'info_82 T_Visibility_48 T_Modality_68
-- Agda.Builtin.Reflection.Arg
d_Arg_88 :: p -> p -> ()
d_Arg_88 p
a0 p
a1 = ()
data T_Arg_88 = C_arg_98 T_ArgInfo_76 AgdaAny
-- Agda.Builtin.Reflection.Blocker
d_Blocker_100 :: ()
d_Blocker_100 = ()
data T_Blocker_100
  = C_blockerAny_102 [T_Blocker_100] |
    C_blockerAll_104 [T_Blocker_100] | C_blockerMeta_106 AgdaAny
-- Agda.Builtin.Reflection.Abs
d_Abs_112 :: p -> p -> ()
d_Abs_112 p
a0 p
a1 = ()
data T_Abs_112
  = C_abs_122 MAlonzo.Code.Agda.Builtin.String.T_String_6 AgdaAny
-- Agda.Builtin.Reflection.Literal
d_Literal_124 :: ()
d_Literal_124 = ()
data T_Literal_124
  = C_nat_128 Integer | C_word64_132 MAlonzo.RTE.Word64 |
    C_float_136 MAlonzo.Code.Agda.Builtin.Float.T_Float_6 |
    C_char_140 MAlonzo.Code.Agda.Builtin.Char.T_Char_6 |
    C_string_144 MAlonzo.Code.Agda.Builtin.String.T_String_6 |
    C_name_148 AgdaAny | C_meta_152 AgdaAny
-- Agda.Builtin.Reflection.Term
d_Term_154 :: ()
d_Term_154 = ()
data T_Term_154
  = C_var_172 Integer [T_Arg_88] | C_con_178 AgdaAny [T_Arg_88] |
    C_def_184 AgdaAny [T_Arg_88] |
    C_lam_190 T_Visibility_48 T_Abs_112 |
    C_pat'45'lam_196 [T_Clause_160] [T_Arg_88] |
    C_pi_202 T_Arg_88 T_Abs_112 | C_agda'45'sort_206 T_Sort_156 |
    C_lit_210 T_Literal_124 | C_meta_214 AgdaAny [T_Arg_88] |
    C_unknown_216
-- Agda.Builtin.Reflection.Sort
d_Sort_156 :: ()
d_Sort_156 = ()
data T_Sort_156
  = C_set_220 T_Term_154 | C_lit_224 Integer |
    C_prop_228 T_Term_154 | C_propLit_232 Integer | C_inf_236 Integer |
    C_unknown_238
-- Agda.Builtin.Reflection.Pattern
d_Pattern_158 :: ()
d_Pattern_158 = ()
data T_Pattern_158
  = C_con_244 AgdaAny [T_Arg_88] | C_dot_248 T_Term_154 |
    C_var_252 Integer | C_lit_256 T_Literal_124 | C_proj_260 AgdaAny |
    C_absurd_264 Integer
-- Agda.Builtin.Reflection.Clause
d_Clause_160 :: ()
d_Clause_160 = ()
data T_Clause_160
  = C_clause_272 [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] [T_Arg_88]
                 T_Term_154 |
    C_absurd'45'clause_278 [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14]
                           [T_Arg_88]
-- Agda.Builtin.Reflection.Type
d_Type_162 :: ()
d_Type_162 :: ()
d_Type_162 = ()
forall a. a
erased
-- Agda.Builtin.Reflection.Telescope
d_Telescope_164 :: ()
d_Telescope_164 :: ()
d_Telescope_164 = ()
forall a. a
erased
-- Agda.Builtin.Reflection.Definition
d_Definition_280 :: ()
d_Definition_280 = ()
data T_Definition_280
  = C_function_284 [T_Clause_160] |
    C_data'45'type_290 Integer [AgdaAny] |
    C_record'45'type_296 AgdaAny [T_Arg_88] |
    C_data'45'cons_302 AgdaAny T_Quantity_62 | C_axiom_304 |
    C_prim'45'fun_306
-- Agda.Builtin.Reflection.ErrorPart
d_ErrorPart_308 :: ()
d_ErrorPart_308 = ()
data T_ErrorPart_308
  = C_strErr_310 MAlonzo.Code.Agda.Builtin.String.T_String_6 |
    C_termErr_312 T_Term_154 | C_pattErr_314 T_Pattern_158 |
    C_nameErr_316 AgdaAny
-- Agda.Builtin.Reflection.TC
d_TC_320 :: a
d_TC_320
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Agda.Builtin.Reflection.TC"
-- Agda.Builtin.Reflection.returnTC
d_returnTC_326 :: a
d_returnTC_326 = a
forall a. a
erased
-- Agda.Builtin.Reflection.bindTC
d_bindTC_336 :: a
d_bindTC_336 = a
forall a. a
erased
-- Agda.Builtin.Reflection.unify
d_unify_338 :: a
d_unify_338 = a
forall a. a
erased
-- Agda.Builtin.Reflection.typeError
d_typeError_344 :: a
d_typeError_344 = a
forall a. a
erased
-- Agda.Builtin.Reflection.inferType
d_inferType_346 :: a
d_inferType_346 = a
forall a. a
erased
-- Agda.Builtin.Reflection.checkType
d_checkType_348 :: a
d_checkType_348 = a
forall a. a
erased
-- Agda.Builtin.Reflection.normalise
d_normalise_350 :: a
d_normalise_350 = a
forall a. a
erased
-- Agda.Builtin.Reflection.reduce
d_reduce_352 :: a
d_reduce_352 = a
forall a. a
erased
-- Agda.Builtin.Reflection.catchTC
d_catchTC_358 :: a
d_catchTC_358 = a
forall a. a
erased
-- Agda.Builtin.Reflection.quoteTC
d_quoteTC_364 :: a
d_quoteTC_364 = a
forall a. a
erased
-- Agda.Builtin.Reflection.unquoteTC
d_unquoteTC_370 :: a
d_unquoteTC_370 = a
forall a. a
erased
-- Agda.Builtin.Reflection.quoteωTC
d_quoteωTC_374 :: a
d_quoteωTC_374 = a
forall a. a
erased
-- Agda.Builtin.Reflection.getContext
d_getContext_376 :: a
d_getContext_376 = a
forall a. a
erased
-- Agda.Builtin.Reflection.extendContext
d_extendContext_382 :: a
d_extendContext_382 = a
forall a. a
erased
-- Agda.Builtin.Reflection.inContext
d_inContext_388 :: a
d_inContext_388 = a
forall a. a
erased
-- Agda.Builtin.Reflection.freshName
d_freshName_390 :: a
d_freshName_390 = a
forall a. a
erased
-- Agda.Builtin.Reflection.declareDef
d_declareDef_392 :: a
d_declareDef_392 = a
forall a. a
erased
-- Agda.Builtin.Reflection.declarePostulate
d_declarePostulate_394 :: a
d_declarePostulate_394 = a
forall a. a
erased
-- Agda.Builtin.Reflection.declareData
d_declareData_396 :: a
d_declareData_396 = a
forall a. a
erased
-- Agda.Builtin.Reflection.defineData
d_defineData_402 :: a
d_defineData_402 = a
forall a. a
erased
-- Agda.Builtin.Reflection.defineFun
d_defineFun_404 :: a
d_defineFun_404 = a
forall a. a
erased
-- Agda.Builtin.Reflection.getType
d_getType_406 :: a
d_getType_406 = a
forall a. a
erased
-- Agda.Builtin.Reflection.getDefinition
d_getDefinition_408 :: a
d_getDefinition_408 = a
forall a. a
erased
-- Agda.Builtin.Reflection.blockTC
d_blockTC_414 :: a
d_blockTC_414 = a
forall a. a
erased
-- Agda.Builtin.Reflection.commitTC
d_commitTC_416 :: a
d_commitTC_416 = a
forall a. a
erased
-- Agda.Builtin.Reflection.isMacro
d_isMacro_418 :: a
d_isMacro_418 = a
forall a. a
erased
-- Agda.Builtin.Reflection.pragmaForeign
d_pragmaForeign_420 :: a
d_pragmaForeign_420 = a
forall a. a
erased
-- Agda.Builtin.Reflection.pragmaCompile
d_pragmaCompile_422 :: a
d_pragmaCompile_422 = a
forall a. a
erased
-- Agda.Builtin.Reflection.withNormalisation
d_withNormalisation_428 :: a
d_withNormalisation_428 = a
forall a. a
erased
-- Agda.Builtin.Reflection.askNormalisation
d_askNormalisation_430 :: a
d_askNormalisation_430 = a
forall a. a
erased
-- Agda.Builtin.Reflection.withReconstructed
d_withReconstructed_436 :: a
d_withReconstructed_436 = a
forall a. a
erased
-- Agda.Builtin.Reflection.askReconstructed
d_askReconstructed_438 :: a
d_askReconstructed_438 = a
forall a. a
erased
-- Agda.Builtin.Reflection.withExpandLast
d_withExpandLast_444 :: a
d_withExpandLast_444 = a
forall a. a
erased
-- Agda.Builtin.Reflection.askExpandLast
d_askExpandLast_446 :: a
d_askExpandLast_446 = a
forall a. a
erased
-- Agda.Builtin.Reflection.withReduceDefs
d_withReduceDefs_454 :: a
d_withReduceDefs_454 = a
forall a. a
erased
-- Agda.Builtin.Reflection.askReduceDefs
d_askReduceDefs_458 :: a
d_askReduceDefs_458 = a
forall a. a
erased
-- Agda.Builtin.Reflection.formatErrorParts
d_formatErrorParts_460 :: a
d_formatErrorParts_460 = a
forall a. a
erased
-- Agda.Builtin.Reflection.debugPrint
d_debugPrint_462 :: a
d_debugPrint_462 = a
forall a. a
erased
-- Agda.Builtin.Reflection.noConstraints
d_noConstraints_468 :: a
d_noConstraints_468 = a
forall a. a
erased
-- Agda.Builtin.Reflection.workOnTypes
d_workOnTypes_474 :: a
d_workOnTypes_474 = a
forall a. a
erased
-- Agda.Builtin.Reflection.runSpeculative
d_runSpeculative_482 :: a
d_runSpeculative_482 = a
forall a. a
erased
-- Agda.Builtin.Reflection.getInstances
d_getInstances_484 :: a
d_getInstances_484 = a
forall a. a
erased
-- Agda.Builtin.Reflection.solveInstanceConstraints
d_solveInstanceConstraints_486 :: a
d_solveInstanceConstraints_486 = a
forall a. a
erased
-- Agda.Builtin.Reflection.filter
d_filter_488 :: (AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny]
d_filter_488 :: (AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny]
d_filter_488 AgdaAny -> Bool
v0 [AgdaAny]
v1
  = case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
      [] -> [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1
      (:) AgdaAny
v2 [AgdaAny]
v3
        -> let v4 :: t
v4 = (AgdaAny -> Bool) -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> Bool
v0 AgdaAny
v2 in
           AgdaAny -> [AgdaAny]
forall a b. a -> b
coe
             (if AgdaAny -> Bool
forall a b. a -> b
coe AgdaAny
forall a. a
v4
                then (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
forall a b. a -> b
coe AgdaAny
v2)
                       (((AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny]
d_filter_488 ((AgdaAny -> Bool) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Bool
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3))
                else ((AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny]
d_filter_488 ((AgdaAny -> Bool) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Bool
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3))
      [AgdaAny]
_ -> [AgdaAny]
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Agda.Builtin.Reflection._∈_
d__'8712'__514 :: AgdaAny -> [AgdaAny] -> Bool
d__'8712'__514 :: AgdaAny -> [AgdaAny] -> Bool
d__'8712'__514 AgdaAny
v0 [AgdaAny]
v1
  = case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
      [] -> Bool -> Bool
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
      (:) AgdaAny
v2 [AgdaAny]
v3
        -> let v4 :: t
v4 = (QName -> QName -> Bool) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe QName -> QName -> Bool
d_primQNameEquality_8 AgdaAny
v0 AgdaAny
v2 in
           AgdaAny -> Bool
forall a b. a -> b
coe
             (if AgdaAny -> Bool
forall a b. a -> b
coe AgdaAny
forall a. a
v4 then AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4 else (AgdaAny -> [AgdaAny] -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> [AgdaAny] -> Bool
d__'8712'__514 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3))
      [AgdaAny]
_ -> Bool
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Agda.Builtin.Reflection._∉_
d__'8713'__540 :: AgdaAny -> [AgdaAny] -> Bool
d__'8713'__540 :: AgdaAny -> [AgdaAny] -> Bool
d__'8713'__540 AgdaAny
v0 [AgdaAny]
v1
  = let v2 :: Bool
v2 = AgdaAny -> [AgdaAny] -> Bool
d__'8712'__514 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0) ([AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1) in
    AgdaAny -> Bool
forall a b. a -> b
coe
      (if Bool -> Bool
forall a b. a -> b
coe Bool
v2
         then Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
         else Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
-- Agda.Builtin.Reflection._++_
d__'43''43'__558 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny]
d__'43''43'__558 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny]
d__'43''43'__558 [AgdaAny]
v0 [AgdaAny]
v1
  = case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v0 of
      [] -> [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1
      (:) AgdaAny
v2 [AgdaAny]
v3
        -> (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
forall a b. a -> b
coe AgdaAny
v2)
             (([AgdaAny] -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> [AgdaAny] -> [AgdaAny]
d__'43''43'__558 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1))
      [AgdaAny]
_ -> [AgdaAny]
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Agda.Builtin.Reflection.combineReduceDefs
d_combineReduceDefs_574 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_combineReduceDefs_574 :: T_Σ_14 -> T_Σ_14 -> T_Σ_14
d_combineReduceDefs_574 T_Σ_14
v0 T_Σ_14
v1
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v2 AgdaAny
v3
        -> if AgdaAny -> Bool
forall a b. a -> b
coe AgdaAny
v2
             then case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v1 of
                    MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v4 AgdaAny
v5
                      -> if AgdaAny -> Bool
forall a b. a -> b
coe AgdaAny
v4
                           then (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                                  AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)
                                  (((AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     (AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny]
d_filter_488 ((AgdaAny -> Bool) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v6 -> AgdaAny -> [AgdaAny] -> Bool
d__'8712'__514 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6) (AgdaAny -> [AgdaAny]
forall a b. a -> b
coe AgdaAny
v3)))
                                     (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
                           else (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                                  AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
                                  (((AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     (AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny]
d_filter_488 ((AgdaAny -> Bool) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v6 -> AgdaAny -> [AgdaAny] -> Bool
d__'8713'__540 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6) (AgdaAny -> [AgdaAny]
forall a b. a -> b
coe AgdaAny
v5)))
                                     (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))
                    T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
             else (case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v1 of
                     MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v4 AgdaAny
v5
                       -> if AgdaAny -> Bool
forall a b. a -> b
coe AgdaAny
v4
                            then (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                                   AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)
                                   (((AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                      (AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny]
d_filter_488 ((AgdaAny -> Bool) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v6 -> AgdaAny -> [AgdaAny] -> Bool
d__'8713'__540 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6) (AgdaAny -> [AgdaAny]
forall a b. a -> b
coe AgdaAny
v3)))
                                      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
                            else (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                                   AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)
                                   (([AgdaAny] -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> [AgdaAny] -> [AgdaAny]
d__'43''43'__558 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
                     T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError)
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Agda.Builtin.Reflection.onlyReduceDefs
d_onlyReduceDefs_602 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> [AgdaAny] -> AgdaAny -> AgdaAny
d_onlyReduceDefs_602 :: () -> () -> [AgdaAny] -> AgdaAny -> AgdaAny
d_onlyReduceDefs_602 ()
v0 ~()
v1 [AgdaAny]
v2 AgdaAny
v3 = () -> [AgdaAny] -> AgdaAny -> AgdaAny
du_onlyReduceDefs_602 ()
v0 [AgdaAny]
v2 AgdaAny
v3
du_onlyReduceDefs_602 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  [AgdaAny] -> AgdaAny -> AgdaAny
du_onlyReduceDefs_602 :: () -> [AgdaAny] -> AgdaAny -> AgdaAny
du_onlyReduceDefs_602 ()
v0 [AgdaAny]
v1 AgdaAny
v2
  = AgdaAny
-> ()
-> ()
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
      AgdaAny
forall a. a
d_bindTC_336 () ()
v0 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
d_askReduceDefs_458
      (\ AgdaAny
v3 ->
         AgdaAny -> () -> AgdaAny -> T_Σ_14 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           AgdaAny
forall a. a
d_withReduceDefs_454 ()
v0 AgdaAny
forall a. a
erased
           (T_Σ_14 -> T_Σ_14 -> T_Σ_14
d_combineReduceDefs_574
              ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                 AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1))
              (AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v3))
           AgdaAny
v2)
-- Agda.Builtin.Reflection.dontReduceDefs
d_dontReduceDefs_608 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> [AgdaAny] -> AgdaAny -> AgdaAny
d_dontReduceDefs_608 :: () -> () -> [AgdaAny] -> AgdaAny -> AgdaAny
d_dontReduceDefs_608 ()
v0 ~()
v1 [AgdaAny]
v2 AgdaAny
v3 = () -> [AgdaAny] -> AgdaAny -> AgdaAny
du_dontReduceDefs_608 ()
v0 [AgdaAny]
v2 AgdaAny
v3
du_dontReduceDefs_608 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  [AgdaAny] -> AgdaAny -> AgdaAny
du_dontReduceDefs_608 :: () -> [AgdaAny] -> AgdaAny -> AgdaAny
du_dontReduceDefs_608 ()
v0 [AgdaAny]
v1 AgdaAny
v2
  = AgdaAny
-> ()
-> ()
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
      AgdaAny
forall a. a
d_bindTC_336 () ()
v0 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
d_askReduceDefs_458
      (\ AgdaAny
v3 ->
         AgdaAny -> () -> AgdaAny -> T_Σ_14 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           AgdaAny
forall a. a
d_withReduceDefs_454 ()
v0 AgdaAny
forall a. a
erased
           (T_Σ_14 -> T_Σ_14 -> T_Σ_14
d_combineReduceDefs_574
              ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                 AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1))
              (AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v3))
           AgdaAny
v2)
-- Agda.Builtin.Reflection.blockOnMeta
d_blockOnMeta_626 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> AgdaAny -> AgdaAny
d_blockOnMeta_626 :: () -> () -> AgdaAny -> AgdaAny
d_blockOnMeta_626 ()
v0 ~()
v1 AgdaAny
v2 = () -> AgdaAny -> AgdaAny
du_blockOnMeta_626 ()
v0 AgdaAny
v2
du_blockOnMeta_626 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> AgdaAny -> AgdaAny
du_blockOnMeta_626 :: () -> AgdaAny -> AgdaAny
du_blockOnMeta_626 ()
v0 AgdaAny
v1
  = AgdaAny -> () -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
d_blockTC_414 ()
v0 AgdaAny
forall a. a
erased ((AgdaAny -> T_Blocker_100) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Blocker_100
C_blockerMeta_106 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))