Documentation

d_SimplifierTag_4 ∷ () Source #

type T_SimplifierTag_4 = SimplifierStage Source #

pattern C_floatDelayT_6 ∷ SimplifierStage Source #

pattern C_forceDelayT_8 ∷ SimplifierStage Source #

pattern C_forceCaseDelayT_10 ∷ SimplifierStage Source #

pattern C_caseOfCaseT_12 ∷ SimplifierStage Source #

pattern C_caseReduceT_14 ∷ SimplifierStage Source #

pattern C_inlineT_16 ∷ SimplifierStage Source #

pattern C_cseT_18 ∷ SimplifierStage Source #

check_floatDelayT_6 ∷ T_SimplifierTag_4 Source #

check_forceDelayT_8 ∷ T_SimplifierTag_4 Source #

check_forceCaseDelayT_10 ∷ T_SimplifierTag_4 Source #

check_caseOfCaseT_12 ∷ T_SimplifierTag_4 Source #

check_caseReduceT_14 ∷ T_SimplifierTag_4 Source #

check_inlineT_16 ∷ T_SimplifierTag_4 Source #

check_cseT_18 ∷ T_SimplifierTag_4 Source #

cover_SimplifierTag_4 ∷ SimplifierStage → () Source #

d_InlineHints_20 ∷ () Source #

type T_InlineHints_20 = Inline Source #

pattern C_var_22 ∷ Inline Source #

pattern C_expand_24 ∷ Inline → Inline Source #

pattern C_ƛ_26 ∷ Inline → Inline Source #

pattern C__'183'__28 ∷ Inline → Inline → Inline Source #

pattern C__'183''8595'_30 ∷ Inline → Inline Source #

pattern C_force_32 ∷ Inline → Inline Source #

pattern C_delay_34 ∷ Inline → Inline Source #

pattern C_con_36 ∷ Inline Source #

pattern C_builtin_38 ∷ Inline Source #

pattern C_error_40 ∷ Inline Source #

pattern C_constr_42 ∷ [Inline] → Inline Source #

pattern C_case_44 ∷ Inline → [Inline] → Inline Source #

check_var_22 ∷ T_InlineHints_20 Source #

check_expand_24 ∷ T_InlineHints_20 → T_InlineHints_20 Source #

check_ƛ_26 ∷ T_InlineHints_20 → T_InlineHints_20 Source #

check__'183'__28 ∷ T_InlineHints_20 → T_InlineHints_20 → T_InlineHints_20 Source #

check__'183''8595'_30 ∷ T_InlineHints_20 → T_InlineHints_20 Source #

check_force_32 ∷ T_InlineHints_20 → T_InlineHints_20 Source #

check_delay_34 ∷ T_InlineHints_20 → T_InlineHints_20 Source #

check_con_36 ∷ T_InlineHints_20 Source #

check_builtin_38 ∷ T_InlineHints_20 Source #

check_error_40 ∷ T_InlineHints_20 Source #

check_constr_42 ∷ T_List_10 () T_InlineHints_20 → T_InlineHints_20 Source #

check_case_44 ∷ T_InlineHints_20 → T_List_10 () T_InlineHints_20 → T_InlineHints_20 Source #

cover_InlineHints_20 ∷ Inline → () Source #

d_Hints_46 ∷ () Source #

type T_Hints_46 = Hints Source #

pattern C_inline_48 ∷ Inline → Hints Source #

pattern C_none_50 ∷ Hints Source #

check_inline_48 ∷ T_InlineHints_20 → T_Hints_46 Source #

check_none_50 ∷ T_Hints_46 Source #

cover_Hints_46 ∷ Hints → () Source #

d_CertResult_60 ∷ p → p → () Source #

data T_CertResult_60 Source #

d_ProofOrCE_86 ∷ p → p → () Source #

data T_ProofOrCE_86 Source #

d_Proof'63'_106 ∷ p → p → () Source #

data T_Proof'63'_106 Source #

d__'62''62''61'__128 ∷ T_Level_18 → T_Level_18 → () → () → T_Proof'63'_106 → (AgdaAny → T_Proof'63'_106) → T_Proof'63'_106 Source #

du__'62''62''61'__128 ∷ T_Proof'63'_106 → (AgdaAny → T_Proof'63'_106) → T_Proof'63'_106 Source #

d_decToPCE_148 ∷ () → () → T_SimplifierTag_4 → T_Dec_20 → AgdaAny → AgdaAny → T_ProofOrCE_86 Source #

du_decToPCE_148 ∷ T_SimplifierTag_4 → T_Dec_20 → AgdaAny → AgdaAny → T_ProofOrCE_86 Source #

d_pceToDec_162 ∷ () → T_ProofOrCE_86 → T_Dec_20 Source #

du_pceToDec_162 ∷ T_ProofOrCE_86 → T_Dec_20 Source #

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

d_matchOrCE_196 ∷ () → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_SimplifierTag_4 → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_ProofOrCE_86 Source #

du_matchOrCE_196 ∷ T_SimplifierTag_4 → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_ProofOrCE_86 Source #

d_pcePointwise_238 ∷ () → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_SimplifierTag_4 → (AgdaAny → AgdaAny → T_ProofOrCE_86) → [AgdaAny] → [AgdaAny] → T_ProofOrCE_86 Source #

du_pcePointwise_238 ∷ T_SimplifierTag_4 → (AgdaAny → AgdaAny → T_ProofOrCE_86) → [AgdaAny] → [AgdaAny] → T_ProofOrCE_86 Source #