plutus-metatheory-1.60.0.0: Command line tool for running plutus core programs
Safe HaskellSafe-Inferred
LanguageHaskell2010

MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles

Documentation

d_IndexedSetoid_18 :: p -> p -> p -> p -> () #

newtype T_IndexedSetoid_18 #

Constructors

C_IndexedSetoid'46'constructor_445 T_IsIndexedEquivalence_22 

d_Carrier_34 :: T_IndexedSetoid_18 -> AgdaAny -> () #

d__'8776'__36 :: T_IndexedSetoid_18 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> () #

d_isEquivalence_38 :: T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22 #

d_refl_42 :: T_IndexedSetoid_18 -> AgdaAny -> AgdaAny -> AgdaAny #

d_reflexive_44 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> T_IndexedSetoid_18 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_44 :: T_IndexedSetoid_18 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_46 :: T_IndexedSetoid_18 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_48 :: T_IndexedSetoid_18 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IndexedPreorder_60 :: p -> p -> p -> p -> p -> () #

newtype T_IndexedPreorder_60 #

Constructors

C_IndexedPreorder'46'constructor_1987 T_IsIndexedPreorder_44 

d_Carrier_80 :: T_IndexedPreorder_60 -> AgdaAny -> () #

d__'8776'__82 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> () #

d__'8818'__84 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> () #

d_isPreorder_86 :: T_IndexedPreorder_60 -> T_IsIndexedPreorder_44 #

d_isEquivalence_90 :: T_IndexedPreorder_60 -> T_IsIndexedEquivalence_22 #

d_refl_92 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny #

du_refl_92 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny #

d_reflexive_94 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_96 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_refl_100 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_reflexive_102 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_104 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_106 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8764'__108 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> () #