| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.Construct.Add.Extrema.Equality
Documentation
d__'8776''8729'__22 ∷ p → p → p → p → p → p → () Source #
d__'8776''8729'__54 ∷ p → p → p → p → p → p → () Source #
d_'91''8776''93''45'injective_96 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T__'8776''8729'__20 → AgdaAny Source #
d_'8776''177''45'refl_98 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 Source #
du_'8776''177''45'refl_98 ∷ (AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 Source #
d_'8776''177''45'sym_100 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 → T__'8776''8729'__20 Source #
du_'8776''177''45'sym_100 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 → T__'8776''8729'__20 Source #
d_'8776''177''45'trans_102 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 → T__'8776''8729'__20 → T__'8776''8729'__20 Source #
du_'8776''177''45'trans_102 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 → T__'8776''8729'__20 → T__'8776''8729'__20 Source #
d_'8776''177''45'dec_104 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T_Dec_32 Source #
du_'8776''177''45'dec_104 ∷ (AgdaAny → AgdaAny → T_Dec_32) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T_Dec_32 Source #
d_'8776''177''45'irrelevant_106 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 → T__'8776''8729'__20 → T__'8801'__12 Source #
d_'8776''177''45'substitutive_110 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → ((AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (Maybe (Maybe AgdaAny) → ()) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 → AgdaAny → AgdaAny Source #
du_'8776''177''45'substitutive_110 ∷ ((AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (Maybe (Maybe AgdaAny) → ()) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 → AgdaAny → AgdaAny Source #
d_'8776''177''45'isEquivalence_112 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → T_IsEquivalence_26 Source #
d_'8776''177''45'isDecEquivalence_114 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsDecEquivalence_44 → T_IsDecEquivalence_44 Source #