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_306 ∷ () Source #

data T_ErrorPart_306 Source #

d_TC_318 ∷ a Source #

d_returnTC_324 ∷ a Source #

d_bindTC_334 ∷ a Source #

d_unify_336 ∷ a Source #

d_typeError_342 ∷ a Source #

d_inferType_344 ∷ a Source #

d_checkType_346 ∷ a Source #

d_normalise_348 ∷ a Source #

d_reduce_350 ∷ a Source #

d_catchTC_356 ∷ a Source #

d_quoteTC_362 ∷ a Source #

d_unquoteTC_368 ∷ a Source #

d_quoteωTC_372 ∷ a Source #

d_getContext_374 ∷ a Source #

d_extendContext_380 ∷ a Source #

d_inContext_386 ∷ a Source #

d_freshName_388 ∷ a Source #

d_declareDef_390 ∷ a Source #

d_declarePostulate_392 ∷ a Source #

d_declareData_394 ∷ a Source #

d_defineData_398 ∷ a Source #

d_defineFun_400 ∷ a Source #

d_getType_402 ∷ a Source #

d_getDefinition_404 ∷ a Source #

d_blockTC_410 ∷ a Source #

d_commitTC_412 ∷ a Source #

d_isMacro_414 ∷ a Source #

d_pragmaForeign_416 ∷ a Source #

d_pragmaCompile_418 ∷ a Source #

d_withNormalisation_424 ∷ a Source #

d_askNormalisation_426 ∷ a Source #

d_withReconstructed_432 ∷ a Source #

d_askReconstructed_434 ∷ a Source #

d_withExpandLast_440 ∷ a Source #

d_askExpandLast_442 ∷ a Source #

d_withReduceDefs_450 ∷ a Source #

d_askReduceDefs_454 ∷ a Source #

d_formatErrorParts_456 ∷ a Source #

d_debugPrint_458 ∷ a Source #

d_noConstraints_464 ∷ a Source #

d_runSpeculative_472 ∷ a Source #

d_getInstances_474 ∷ a Source #

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

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

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

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

d_combineReduceDefs_562 ∷ T_Σ_14 → T_Σ_14 → T_Σ_14 Source #

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

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

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

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

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

du_blockOnMeta_614 ∷ T_Level_18 → AgdaAny → AgdaAny Source #