Documentation

d_Name_6 ∷ a Source #

d_primQNameEquality_8 ∷ QName → QName → Bool Source #

d_primQNameLess_10 ∷ QName → QName → Bool Source #

d_primShowQName_12 ∷ QName → Text Source #

d_Associativity_14 ∷ () Source #

type T_Associativity_14 = Assoc Source #

pattern C_left'45'assoc_16 ∷ Assoc Source #

pattern C_right'45'assoc_18 ∷ Assoc Source #

pattern C_non'45'assoc_20 ∷ Assoc Source #

check_left'45'assoc_16 ∷ T_Associativity_14 Source #

check_right'45'assoc_18 ∷ T_Associativity_14 Source #

check_non'45'assoc_20 ∷ T_Associativity_14 Source #

cover_Associativity_14 ∷ Assoc → () Source #

d_Precedence_22 ∷ () Source #

type T_Precedence_22 = Precedence Source #

pattern C_related_24 ∷ PrecedenceLevel → Precedence Source #

pattern C_unrelated_26 ∷ Precedence Source #

check_related_24 ∷ T_Float_6 → T_Precedence_22 Source #

check_unrelated_26 ∷ T_Precedence_22 Source #

cover_Precedence_22 ∷ Precedence → () Source #

d_Fixity_28 ∷ () Source #

type T_Fixity_28 = Fixity Source #

pattern C_fixity_30 ∷ Assoc → Precedence → Fixity Source #

check_fixity_30 ∷ T_Associativity_14 → T_Precedence_22 → T_Fixity_28 Source #

cover_Fixity_28 ∷ Fixity → () Source #

d_primQNameFixity_32 ∷ QName → Fixity Source #

d_primQNameToWord64s_36 ∷ QName → (Integer, Integer) Source #

d_Meta_38 ∷ a Source #

d_primMetaEquality_40 ∷ (Integer, Integer) → (Integer, Integer) → Bool Source #

d_primMetaLess_42 ∷ (Integer, Integer) → (Integer, Integer) → Bool Source #

d_primShowMeta_44 ∷ (Integer, Integer) → Text Source #

d_primMetaToNat_46 ∷ (Integer, Integer) → Integer Source #

d_Visibility_48 ∷ () Source #

data T_Visibility_48 Source #

d_Relevance_56 ∷ () Source #

data T_Relevance_56 Source #

d_Quantity_62 ∷ () Source #

data T_Quantity_62 Source #

d_Modality_68 ∷ () Source #

data T_Modality_68 Source #

d_ArgInfo_76 ∷ () Source #

data T_ArgInfo_76 Source #

d_Arg_88 ∷ p → p → () Source #

data T_Arg_88 Source #

d_Blocker_100 ∷ () Source #

data T_Blocker_100 Source #

d_Abs_112 ∷ p → p → () Source #

data T_Abs_112 Source #

d_Literal_124 ∷ () Source #

data T_Literal_124 Source #

d_Term_154 ∷ () Source #

data T_Term_154 Source #

d_Sort_156 ∷ () Source #

data T_Sort_156 Source #

d_Pattern_158 ∷ () Source #

data T_Pattern_158 Source #

d_Clause_160 ∷ () Source #

data T_Clause_160 Source #

d_Type_162 ∷ () Source #

d_Telescope_164 ∷ () Source #

d_Definition_280 ∷ () Source #

data T_Definition_280 Source #

d_ErrorPart_308 ∷ () Source #

data T_ErrorPart_308 Source #

d_TC_320 ∷ a Source #

d_returnTC_326 ∷ a Source #

d_bindTC_336 ∷ a Source #

d_unify_338 ∷ a Source #

d_typeError_344 ∷ a Source #

d_inferType_346 ∷ a Source #

d_checkType_348 ∷ a Source #

d_normalise_350 ∷ a Source #

d_reduce_352 ∷ a Source #

d_catchTC_358 ∷ a Source #

d_quoteTC_364 ∷ a Source #

d_unquoteTC_370 ∷ a Source #

d_quoteωTC_374 ∷ a Source #

d_getContext_376 ∷ a Source #

d_extendContext_382 ∷ a Source #

d_inContext_388 ∷ a Source #

d_freshName_390 ∷ a Source #

d_declareDef_392 ∷ a Source #

d_declarePostulate_394 ∷ a Source #

d_declareData_396 ∷ a Source #

d_defineData_402 ∷ a Source #

d_defineFun_404 ∷ a Source #

d_getType_406 ∷ a Source #

d_getDefinition_408 ∷ a Source #

d_blockTC_414 ∷ a Source #

d_commitTC_416 ∷ a Source #

d_isMacro_418 ∷ a Source #

d_pragmaForeign_420 ∷ a Source #

d_pragmaCompile_422 ∷ a Source #

d_withNormalisation_428 ∷ a Source #

d_askNormalisation_430 ∷ a Source #

d_withReconstructed_436 ∷ a Source #

d_askReconstructed_438 ∷ a Source #

d_withExpandLast_444 ∷ a Source #

d_askExpandLast_446 ∷ a Source #

d_withReduceDefs_454 ∷ a Source #

d_askReduceDefs_458 ∷ a Source #

d_formatErrorParts_460 ∷ a Source #

d_debugPrint_462 ∷ a Source #

d_noConstraints_468 ∷ a Source #

d_workOnTypes_474 ∷ a Source #

d_runSpeculative_482 ∷ a Source #

d_getInstances_484 ∷ a Source #

d_solveInstanceConstraints_486 ∷ a Source #

d_filter_488 ∷ (AgdaAny → Bool) → [AgdaAny] → [AgdaAny] Source #

d__'8712'__514 ∷ AgdaAny → [AgdaAny] → Bool Source #

d__'8713'__540 ∷ AgdaAny → [AgdaAny] → Bool Source #

d__'43''43'__558 ∷ [AgdaAny] → [AgdaAny] → [AgdaAny] Source #

d_combineReduceDefs_574 ∷ T_Σ_14 → T_Σ_14 → T_Σ_14 Source #

d_onlyReduceDefs_602 ∷ T_Level_18 → () → [AgdaAny] → AgdaAny → AgdaAny Source #

du_onlyReduceDefs_602 ∷ T_Level_18 → [AgdaAny] → AgdaAny → AgdaAny Source #

d_dontReduceDefs_608 ∷ T_Level_18 → () → [AgdaAny] → AgdaAny → AgdaAny Source #

du_dontReduceDefs_608 ∷ T_Level_18 → [AgdaAny] → AgdaAny → AgdaAny Source #

d_blockOnMeta_626 ∷ T_Level_18 → () → AgdaAny → AgdaAny Source #

du_blockOnMeta_626 ∷ T_Level_18 → AgdaAny → AgdaAny Source #