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

MAlonzo.Code.Relation.Binary.Structures.Biased

Documentation

d_IsEquivalence_30 ∷ p → p → p → p → () Source #

d_IsStrictTotalOrder_40 ∷ p → p → p → p → p → p → () Source #

d_refl_274 ∷ T_IsEquivalence_26 → AgdaAny → AgdaAny Source #

d_sym_278 ∷ T_IsEquivalence_26 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_280 ∷ T_IsEquivalence_26 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_compare_402 ∷ T_IsStrictTotalOrder_534 → AgdaAny → AgdaAny → T_Tri_158 Source #

d_isStrictPartialOrder_412 ∷ T_IsStrictTotalOrder_534 → T_IsStrictPartialOrder_290 Source #

d_IsStrictTotalOrder'7580'_522 ∷ p → p → p → p → p → p → () Source #

data T_IsStrictTotalOrder'7580'_522 Source #

Constructors

C_IsStrictTotalOrder'7580''46'constructor_6029 T_IsEquivalence_26 (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → T_Tri_158) 

d_isEquivalence_532 ∷ T_IsStrictTotalOrder'7580'_522 → T_IsEquivalence_26 Source #

d_trans_534 ∷ T_IsStrictTotalOrder'7580'_522 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_compare_536 ∷ T_IsStrictTotalOrder'7580'_522 → AgdaAny → AgdaAny → T_Tri_158 Source #

d_isStrictTotalOrder'7580'_538 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder'7580'_522 → T_IsStrictTotalOrder_534 Source #

du_isStrictTotalOrder'7580'_538 ∷ T_IsStrictTotalOrder'7580'_522 → T_IsStrictTotalOrder_534 Source #