| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.Reasoning.Base.Double
Documentation
d__IsRelatedTo__62 ∷ p → p → p → p → p → p → p → p → p → () Source #
data T__IsRelatedTo__62 Source #
Constructors
| C_nonstrict_70 AgdaAny | |
| C_equals_74 AgdaAny |
d_start_76 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → T__IsRelatedTo__62 → AgdaAny Source #
d_'8801''45'go_82 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__IsRelatedTo__62 → T__IsRelatedTo__62 Source #
d_'46'extendedlambda0_88 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → T__'8801'__12 → AgdaAny Source #
d_'46'extendedlambda1_94 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → T__'8801'__12 → AgdaAny Source #
d_'8818''45'go_96 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__62 → T__IsRelatedTo__62 Source #
du_'8818''45'go_96 ∷ T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__62 → T__IsRelatedTo__62 Source #
d_'8776''45'go_106 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__62 → T__IsRelatedTo__62 Source #
du_'8776''45'go_106 ∷ T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__62 → T__IsRelatedTo__62 Source #
d_stop_116 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → T__IsRelatedTo__62 Source #
d_IsEquality_122 ∷ p → p → p → p → p → p → p → p → p → p → () Source #
data T_IsEquality_122 Source #
Constructors
| C_isEquality_130 |
d_IsEquality'63'_138 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → T__IsRelatedTo__62 → T_Dec_20 Source #
d_extractEquality_148 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → T__IsRelatedTo__62 → T_IsEquality_122 → AgdaAny Source #
d_equalitySubRelation_152 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → T_SubRelation_60 Source #
d_begin__156 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → T__IsRelatedTo__62 → AgdaAny Source #
d_begin__160 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → T__IsRelatedTo__62 → AgdaAny → AgdaAny Source #
du_begin__160 ∷ AgdaAny → AgdaAny → T__IsRelatedTo__62 → AgdaAny → AgdaAny Source #
d_step'45''8801'_164 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__62 → T__'8801'__12 → T__IsRelatedTo__62 Source #
du_step'45''8801'_164 ∷ AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__62 → T__'8801'__12 → T__IsRelatedTo__62 Source #
d_step'45''8801''45''8739'_166 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → T__IsRelatedTo__62 → T__IsRelatedTo__62 Source #
d_step'45''8801''45''10216'_168 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__62 → T__'8801'__12 → T__IsRelatedTo__62 Source #
du_step'45''8801''45''10216'_168 ∷ AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__62 → T__'8801'__12 → T__IsRelatedTo__62 Source #
d_step'45''8801''45''10217'_170 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__62 → T__'8801'__12 → T__IsRelatedTo__62 Source #
du_step'45''8801''45''10217'_170 ∷ AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__62 → T__'8801'__12 → T__IsRelatedTo__62 Source #
d_step'45''8801''728'_172 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__62 → T__'8801'__12 → T__IsRelatedTo__62 Source #
du_step'45''8801''728'_172 ∷ AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__62 → T__'8801'__12 → T__IsRelatedTo__62 Source #
d_step'45''8776'_176 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__62 → AgdaAny → T__IsRelatedTo__62 Source #
du_step'45''8776'_176 ∷ T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__62 → AgdaAny → T__IsRelatedTo__62 Source #
d_step'45''8776''45''10216'_178 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__62 → AgdaAny → T__IsRelatedTo__62 Source #
du_step'45''8776''45''10216'_178 ∷ T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__62 → AgdaAny → T__IsRelatedTo__62 Source #
d_step'45''8776''45''10217'_180 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__62 → AgdaAny → T__IsRelatedTo__62 Source #
du_step'45''8776''45''10217'_180 ∷ T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__62 → AgdaAny → T__IsRelatedTo__62 Source #
d_step'45''8776''728'_182 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__62 → AgdaAny → T__IsRelatedTo__62 Source #
du_step'45''8776''728'_182 ∷ T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__62 → AgdaAny → T__IsRelatedTo__62 Source #
d_step'45''8818'_186 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__62 → AgdaAny → T__IsRelatedTo__62 Source #
du_step'45''8818'_186 ∷ T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__62 → AgdaAny → T__IsRelatedTo__62 Source #
d__'8718'_190 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → T__IsRelatedTo__62 Source #
d_step'45''8764'_194 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__62 → AgdaAny → T__IsRelatedTo__62 Source #