Documentation

d_CaseReduce_4 ∷ p → p → p → p → () Source #

data T_CaseReduce_4 Source #

d_isCaseReduce'63'_30 ∷ () → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → T_ProofOrCE_26 Source #

du_isCaseReduce'63'_30 ∷ T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → T_ProofOrCE_26 Source #

d_justEq_38 ∷ () → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #

d_isCR'63'_48 ∷ () → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → T_ProofOrCE_26 Source #

du_isCR'63'_48 ∷ T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → T_ProofOrCE_26 Source #

d_'46'extendedlambda0_64 ∷ () → T__'8866'_14 → (T_isCase_574 → T_Irrelevant_20) → T_DecEq_6 → T__'8866'_14 → T_CaseReduce_4 → T_Irrelevant_20 Source #

d_'46'extendedlambda1_92 ∷ () → [T__'8866'_14] → Integer → T__'8801'__12 → [T__'8866'_14] → T_DecEq_6 → T__'8866'_14 → T_CaseReduce_4 → T_Irrelevant_20 Source #

d_'46'extendedlambda2_96 ∷ () → [T__'8866'_14] → Integer → T__'8801'__12 → [T__'8866'_14] → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → T__'8801'__12 → T_Translation_16 → T__'8801'__12 → T_Irrelevant_20 Source #

d_'46'extendedlambda3_148 ∷ () → T__'8866'_14 → [T__'8866'_14] → T_DecEq_6 → T__'8866'_14 → (T_Translation_16 → T_Irrelevant_20) → () → () → T_SimplifierTag_4 → AgdaAny → AgdaAny → [T__'8866'_14] → Integer → T__'8801'__12 → T_CaseReduce_4 → T_Irrelevant_20 Source #

d_UCaseReduce_156 ∷ () → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → () Source #

d_integer_158 ∷ T__'8866''9839'_4 Source #

d_con'45'integer_162 ∷ () → Integer → T__'8866'_14 Source #

du_con'45'integer_162 ∷ Integer → T__'8866'_14 Source #

d_ast'8321'_166 ∷ T__'8866'_14 Source #

d_ast'8321'''_168 ∷ T__'8866'_14 Source #

d_ast_172 ∷ T__'8866'_14 Source #

d_ast''_174 ∷ T__'8866'_14 Source #

d_ex1_176 ∷ T__'8866'_14 Source #

d_ex2_178 ∷ T__'8866'_14 Source #