| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Untyped.Relation.Binary.Properties
Documentation
d_Reflexive_8 ∷ (Integer → T__'8866'_14 → T__'8866'_14 → ()) → () Source #
d_Transitive_16 ∷ (Integer → T__'8866'_14 → T__'8866'_14 → ()) → () Source #
d_Symmetric_28 ∷ (Integer → T__'8866'_14 → T__'8866'_14 → ()) → () Source #
d_Idempotent_38 ∷ (Integer → T__'8866'_14 → T__'8866'_14 → ()) → () Source #
d__'8838'__50 ∷ (Integer → T__'8866'_14 → T__'8866'_14 → ()) → (Integer → T__'8866'_14 → T__'8866'_14 → ()) → () Source #
d_'8838''45'trans_68 ∷ (Integer → T__'8866'_14 → T__'8866'_14 → ()) → (Integer → T__'8866'_14 → T__'8866'_14 → ()) → (Integer → T__'8866'_14 → T__'8866'_14 → ()) → (Integer → T__'8866'_14 → T__'8866'_14 → AgdaAny → AgdaAny) → (Integer → T__'8866'_14 → T__'8866'_14 → AgdaAny → AgdaAny) → Integer → T__'8866'_14 → T__'8866'_14 → AgdaAny → AgdaAny Source #
du_'8838''45'trans_68 ∷ (Integer → T__'8866'_14 → T__'8866'_14 → AgdaAny → AgdaAny) → (Integer → T__'8866'_14 → T__'8866'_14 → AgdaAny → AgdaAny) → Integer → T__'8866'_14 → T__'8866'_14 → AgdaAny → AgdaAny Source #
d_Transform_76 ∷ () Source #
d_Transform'63'_80 ∷ () Source #
d_Transform'8322'_84 ∷ () Source #
d_Deterministic'7523'_88 ∷ (Integer → T__'8866'_14 → T__'8866'_14 → ()) → () Source #
d_Deterministic'8343'_100 ∷ (Integer → T__'8866'_14 → T__'8866'_14 → ()) → () Source #
d_Compatible_112 ∷ (Integer → T__'8866'_14 → T__'8866'_14 → ()) → (Integer → T__'8866'_14 → T__'8866'_14) → () Source #
d_Compatible'8322'_124 ∷ (Integer → T__'8866'_14 → T__'8866'_14 → ()) → (Integer → T__'8866'_14 → T__'8866'_14 → T__'8866'_14) → () Source #
d_pointwise'45'refl_146 ∷ Integer → (Integer → T__'8866'_14 → T__'8866'_14 → ()) → [T__'8866'_14] → (Integer → T__'8866'_14 → AgdaAny) → T_Pointwise_20 Source #
du_pointwise'45'refl_146 ∷ Integer → [T__'8866'_14] → (Integer → T__'8866'_14 → AgdaAny) → T_Pointwise_20 Source #
d_Refines_158 ∷ (Integer → T__'8866'_14 → T__'8866'_14) → (Integer → T__'8866'_14 → T__'8866'_14 → ()) → () Source #
d_Refines'63'_168 ∷ (Integer → T__'8866'_14 → Maybe T__'8866'_14) → (Integer → T__'8866'_14 → T__'8866'_14 → ()) → () Source #
d_Refines'63''45''8838'_188 ∷ (Integer → T__'8866'_14 → Maybe T__'8866'_14) → (Integer → T__'8866'_14 → T__'8866'_14 → ()) → (Integer → T__'8866'_14 → T__'8866'_14 → ()) → (Integer → T__'8866'_14 → T__'8866'_14 → AgdaAny → AgdaAny) → (Integer → T__'8866'_14 → T__'8866'_14 → T__'8801'__12 → AgdaAny) → Integer → T__'8866'_14 → T__'8866'_14 → T__'8801'__12 → AgdaAny Source #
du_Refines'63''45''8838'_188 ∷ (Integer → T__'8866'_14 → T__'8866'_14 → AgdaAny → AgdaAny) → (Integer → T__'8866'_14 → T__'8866'_14 → T__'8801'__12 → AgdaAny) → Integer → T__'8866'_14 → T__'8866'_14 → T__'8801'__12 → AgdaAny Source #
d_Refinement'63'_196 ∷ (Integer → T__'8866'_14 → T__'8866'_14 → ()) → () Source #
d_refine'63'_210 ∷ Integer → (Integer → T__'8866'_14 → T__'8866'_14 → ()) → (Integer → T__'8866'_14 → Maybe T_Σ_14) → T__'8866'_14 → Maybe T__'8866'_14 Source #
du_refine'63'_210 ∷ Integer → (Integer → T__'8866'_14 → Maybe T_Σ_14) → T__'8866'_14 → Maybe T__'8866'_14 Source #
d_refine'63''45'refines_234 ∷ (Integer → T__'8866'_14 → T__'8866'_14 → ()) → (Integer → T__'8866'_14 → Maybe T_Σ_14) → Integer → T__'8866'_14 → T__'8866'_14 → T__'8801'__12 → AgdaAny Source #
du_refine'63''45'refines_234 ∷ (Integer → T__'8866'_14 → Maybe T_Σ_14) → Integer → T__'8866'_14 → AgdaAny Source #