plutus-metatheory-0.1.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_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 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_44 ∷ p → p → p → p → p → p → p → p → () Source #

data T_IsIndexedPreorder_44 Source #

Constructors

C_IsIndexedPreorder'46'constructor_5831 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 Source #

d_reflexive_66 ∷ T_IsIndexedPreorder_44 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_68 ∷ T_IsIndexedPreorder_44 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_refl_72 ∷ T_IsIndexedPreorder_44 → AgdaAny → AgdaAny → AgdaAny Source #

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

du_reflexive_74 ∷ T_IsIndexedPreorder_44 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_76 ∷ T_IsIndexedPreorder_44 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_78 ∷ T_IsIndexedPreorder_44 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_refl_80 ∷ T_IsIndexedPreorder_44 → AgdaAny → AgdaAny → AgdaAny Source #