plutus-metatheory-1.60.0.0: Command line tool for running plutus core programs
Safe HaskellSafe-Inferred
LanguageHaskell2010

MAlonzo.Code.Agda.Builtin.Reflection

Documentation

d_Name_6 :: a #

d_primQNameEquality_8 :: QName -> QName -> Text #

d_primMetaToNat_46 :: (Integer, Integer) -> Integer #

d_Visibility_48 :: () #

data T_Visibility_48 #

Constructors

C_visible_50 
C_hidden_52 
C_instance'8242'_54 

d_Relevance_56 :: () #

data T_Relevance_56 #

Constructors

C_relevant_58 
C_irrelevant_60 

d_Quantity_62 :: () #

data T_Quantity_62 #

Constructors

C_quantity'45'0_64 
C_quantity'45'ω_66 

d_Modality_68 :: () #

data T_Modality_68 #

Constructors

C_modality_74 T_Relevance_56 T_Quantity_62 

d_ArgInfo_76 :: () #

data T_ArgInfo_76 #

Constructors

C_arg'45'info_82 T_Visibility_48 T_Modality_68 

d_Arg_88 :: p -> p -> () #

data T_Arg_88 #

Constructors

C_arg_98 T_ArgInfo_76 AgdaAny 

d_Blocker_100 :: () #

data T_Blocker_100 #

Constructors

C_blockerAny_102 [T_Blocker_100] 
C_blockerAll_104 [T_Blocker_100] 
C_blockerMeta_106 AgdaAny 

d_Abs_112 :: p -> p -> () #

data T_Abs_112 #

Constructors

C_abs_122 T_String_6 AgdaAny 

d_Literal_124 :: () #

data T_Literal_124 #

Constructors

C_nat_128 Integer 
C_word64_132 Word64 
C_float_136 T_Float_6 
C_char_140 T_Char_6 
C_string_144 T_String_6 
C_name_148 AgdaAny 
C_meta_152 AgdaAny 

d_Term_154 :: () #

data T_Term_154 #

Constructors

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 

d_Sort_156 :: () #

data T_Sort_156 #

Constructors

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 

d_Pattern_158 :: () #

data T_Pattern_158 #

Constructors

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 

d_Clause_160 :: () #

data T_Clause_160 #

Constructors

C_clause_272 [T_Σ_14] [T_Arg_88] T_Term_154 
C_absurd'45'clause_278 [T_Σ_14] [T_Arg_88] 

d_Type_162 :: () #

d_Telescope_164 :: () #

d_Definition_280 :: () #

data T_Definition_280 #

Constructors

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 

d_ErrorPart_308 :: () #

data T_ErrorPart_308 #

Constructors

C_strErr_310 T_String_6 
C_termErr_312 T_Term_154 
C_pattErr_314 T_Pattern_158 
C_nameErr_316 AgdaAny 

d_TC_320 :: a #

d_returnTC_326 :: a #

d_bindTC_336 :: a #

d_unify_338 :: a #

d_typeError_344 :: a #

d_inferType_346 :: a #

d_checkType_348 :: a #

d_normalise_350 :: a #

d_reduce_352 :: a #

d_catchTC_358 :: a #

d_quoteTC_364 :: a #

d_unquoteTC_370 :: a #

d_quoteωTC_374 :: a #

d_getContext_376 :: a #

d_extendContext_382 :: a #

d_inContext_388 :: a #

d_freshName_390 :: a #

d_declareDef_392 :: a #

d_declarePostulate_394 :: a #

d_declareData_396 :: a #

d_defineData_402 :: a #

d_defineFun_404 :: a #

d_getType_406 :: a #

d_getDefinition_408 :: a #

d_blockTC_414 :: a #

d_commitTC_416 :: a #

d_isMacro_418 :: a #

d_pragmaForeign_420 :: a #

d_pragmaCompile_422 :: a #

d_withNormalisation_428 :: a #

d_askNormalisation_430 :: a #

d_withReconstructed_436 :: a #

d_askReconstructed_438 :: a #

d_withExpandLast_444 :: a #

d_askExpandLast_446 :: a #

d_withReduceDefs_454 :: a #

d_askReduceDefs_458 :: a #

d_formatErrorParts_460 :: a #

d_debugPrint_462 :: a #

d_noConstraints_468 :: a #

d_workOnTypes_474 :: a #

d_runSpeculative_482 :: a #

d_getInstances_484 :: a #

d_solveInstanceConstraints_486 :: a #

d_filter_488 :: (AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny] #

d__'8712'__514 :: AgdaAny -> [AgdaAny] -> Bool #

d__'8713'__540 :: AgdaAny -> [AgdaAny] -> Bool #

d__'43''43'__558 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny] #

d_combineReduceDefs_574 :: T_Σ_14 -> T_Σ_14 -> T_Σ_14 #

d_onlyReduceDefs_602 :: T_Level_18 -> () -> [AgdaAny] -> AgdaAny -> AgdaAny #

du_onlyReduceDefs_602 :: T_Level_18 -> [AgdaAny] -> AgdaAny -> AgdaAny #

d_dontReduceDefs_608 :: T_Level_18 -> () -> [AgdaAny] -> AgdaAny -> AgdaAny #

du_dontReduceDefs_608 :: T_Level_18 -> [AgdaAny] -> AgdaAny -> AgdaAny #

d_blockOnMeta_626 :: T_Level_18 -> () -> AgdaAny -> AgdaAny #

du_blockOnMeta_626 :: T_Level_18 -> AgdaAny -> AgdaAny #