| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Algebra.Consequences.Base
Documentation
d_Congruent'8322'_24 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_LeftCongruent_30 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_RightCongruent_32 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_'8729''45'cong'737'_42 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8729''45'cong'737'_42 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8729''45'cong'691'_46 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8729''45'cong'691'_46 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_Idempotent_68 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Selective_76 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_sel'8658'idem_80 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → AgdaAny Source #
du_sel'8658'idem_80 ∷ (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → AgdaAny Source #
d_Involutive_106 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → () Source #
d_SelfInverse_114 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → () Source #
d_reflexive'8743'selfInverse'8658'involutive_116 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_reflexive'8743'selfInverse'8658'involutive_116 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #