plutus-metatheory-1.70.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 → () Source #

data T_IsIndexedEquivalence_22 Source #

Constructors

C_constructor_40 (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 Source #

d_sym_32 ∷ T_IsIndexedEquivalence_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_34 ∷ T_IsIndexedEquivalence_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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 Source #

du_reflexive_38 ∷ T_IsIndexedEquivalence_22 → AgdaAny → AgdaAny → AgdaAny Source #

d_IsIndexedPreorder_46 ∷ p → p → p → p → p → p → p → p → () Source #

data T_IsIndexedPreorder_46 Source #

Constructors

C_constructor_84 T_IsIndexedEquivalence_22 (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) 

d_isEquivalence_62 ∷ T_IsIndexedPreorder_46 → T_IsIndexedEquivalence_22 Source #

d_reflexive_68 ∷ T_IsIndexedPreorder_46 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_70 ∷ T_IsIndexedPreorder_46 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_refl_74 ∷ T_IsIndexedPreorder_46 → AgdaAny → AgdaAny → AgdaAny Source #

d_reflexive_76 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → ()) → T_IsIndexedPreorder_46 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_76 ∷ T_IsIndexedPreorder_46 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_78 ∷ T_IsIndexedPreorder_46 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_80 ∷ T_IsIndexedPreorder_46 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_refl_82 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → ()) → T_IsIndexedPreorder_46 → AgdaAny → AgdaAny → AgdaAny Source #

du_refl_82 ∷ T_IsIndexedPreorder_46 → AgdaAny → AgdaAny → AgdaAny Source #