plutus-metatheory-0.1.0.0: Command line tool for running plutus core programs

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_IndexedSetoid'46'constructor_445 T_IsIndexedEquivalence_22

d_Carrier_34 ∷ T_IndexedSetoid_18 → AgdaAny → () Source #

d__'8776'__36 ∷ T_IndexedSetoid_18 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → () Source #

d_isEquivalence_38 ∷ T_IndexedSetoid_18 → T_IsIndexedEquivalence_22 Source #

d_refl_42 ∷ T_IndexedSetoid_18 → 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_sym_46 ∷ T_IndexedSetoid_18 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_48 ∷ T_IndexedSetoid_18 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IndexedPreorder_60 ∷ p → p → p → p → p → () Source #

newtype T_IndexedPreorder_60 Source #

Constructors

C_IndexedPreorder'46'constructor_1987 T_IsIndexedPreorder_44

d_Carrier_80 ∷ T_IndexedPreorder_60 → AgdaAny → () Source #

d__'8776'__82 ∷ T_IndexedPreorder_60 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → () Source #

d__'8818'__84 ∷ T_IndexedPreorder_60 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → () Source #

d_isPreorder_86 ∷ T_IndexedPreorder_60 → T_IsIndexedPreorder_44 Source #

d_isEquivalence_90 ∷ T_IndexedPreorder_60 → T_IsIndexedEquivalence_22 Source #

d_refl_92 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → T_Level_18 → T_IndexedPreorder_60 → AgdaAny → AgdaAny → AgdaAny Source #

du_refl_92 ∷ T_IndexedPreorder_60 → AgdaAny → AgdaAny → AgdaAny Source #

d_reflexive_94 ∷ T_IndexedPreorder_60 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_96 ∷ T_IndexedPreorder_60 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_refl_100 ∷ T_IndexedPreorder_60 → AgdaAny → AgdaAny → AgdaAny Source #

d_reflexive_102 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → T_Level_18 → T_IndexedPreorder_60 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_102 ∷ T_IndexedPreorder_60 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_104 ∷ T_IndexedPreorder_60 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_106 ∷ T_IndexedPreorder_60 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8764'__108 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → T_Level_18 → T_IndexedPreorder_60 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → () Source #