| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles
Documentation
d_IndexedSetoid_18 ∷ p → p → p → p → () Source #
newtype T_IndexedSetoid_18 Source #
Constructors
| C_constructor_50 T_IsIndexedEquivalence_22 |
d_Carrier_34 ∷ T_IndexedSetoid_18 → AgdaAny → () Source #
d__'8776'__36 ∷ T_IndexedSetoid_18 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → () Source #
d_reflexive_44 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → T_IndexedSetoid_18 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #
du_reflexive_44 ∷ T_IndexedSetoid_18 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #
d_trans_48 ∷ T_IndexedSetoid_18 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_IndexedPreorder_62 ∷ p → p → p → p → p → () Source #
newtype T_IndexedPreorder_62 Source #
Constructors
| C_constructor_112 T_IsIndexedPreorder_46 |
d_Carrier_82 ∷ T_IndexedPreorder_62 → AgdaAny → () Source #
d__'8776'__84 ∷ T_IndexedPreorder_62 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → () Source #
d__'8818'__86 ∷ T_IndexedPreorder_62 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → () Source #
d_refl_94 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → T_Level_18 → T_IndexedPreorder_62 → AgdaAny → AgdaAny → AgdaAny Source #
d_reflexive_96 ∷ T_IndexedPreorder_62 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_trans_98 ∷ T_IndexedPreorder_62 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_reflexive_104 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → T_Level_18 → T_IndexedPreorder_62 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #
du_reflexive_104 ∷ T_IndexedPreorder_62 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #
d_sym_106 ∷ T_IndexedPreorder_62 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_trans_108 ∷ T_IndexedPreorder_62 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d__'8764'__110 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → T_Level_18 → T_IndexedPreorder_62 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → () Source #