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

MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures

Documentation

d_IsIndexedEquivalence_22 :: p -> p -> p -> p -> p -> p -> () #

data T_IsIndexedEquivalence_22 #

Constructors

C_IsIndexedEquivalence'46'constructor_1089 (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) 

d_refl_30 :: T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny #

d_sym_32 :: T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_34 :: T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_reflexive_38 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()) -> T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_38 :: T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsIndexedPreorder_44 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsIndexedPreorder_44 #

Constructors

C_IsIndexedPreorder'46'constructor_5837 T_IsIndexedEquivalence_22 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) 

d_isEquivalence_60 :: T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22 #

d_reflexive_66 :: T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_68 :: T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_refl_72 :: T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny #

d_reflexive_74 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()) -> T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_74 :: T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_sym_76 :: T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_78 :: T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_refl_80 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()) -> T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny #

du_refl_80 :: T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny #