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

MAlonzo.Code.Relation.Binary.Consequences

Documentation

d_subst'8658'resp'737'_38T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → ((AgdaAny → ()) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

du_subst'8658'resp'737'_38 ∷ (AgdaAnyAgdaAny → ()) → ((AgdaAny → ()) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_subst'8658'resp'691'_48T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → ((AgdaAny → ()) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

du_subst'8658'resp'691'_48 ∷ (AgdaAnyAgdaAny → ()) → ((AgdaAny → ()) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_subst'8658'resp'8322'_58T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → ((AgdaAny → ()) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → T_Σ_14 Source #

d_resp'8658''172''45'resp_76T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyAgdaAny → (AgdaAnyT_'8869'_4) → AgdaAnyT_'8869'_4 Source #

d_total'8658'refl_102T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → T_Σ_14 → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyT__'8846'__30) → AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_total'8743'dec'8658'dec_154T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyT__'8846'__30) → (AgdaAnyAgdaAnyT_Dec_32) → AgdaAnyAgdaAnyT_Dec_32 Source #

d_mono'8658'cong_226T_Level_18 → () → T_Level_18T_Level_18 → () → T_Level_18T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

du_mono'8658'cong_226 ∷ (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_antimono'8658'cong_240T_Level_18 → () → T_Level_18T_Level_18 → () → T_Level_18T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_trans'8743'irr'8658'asym_266T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyT_'8869'_4) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyT_'8869'_4 Source #

d_irr'8743'antisym'8658'asym_278T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyT_'8869'_4) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyT_'8869'_4 Source #

d_asym'8658'antisym_288T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyT_'8869'_4) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_asym'8658'irr_296T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → T_Σ_14 → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyT_'8869'_4) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyT_'8869'_4 Source #

d_tri'8658'asym_314T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyT_Tri_136) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyT_'8869'_4 Source #

d_tri'8658'irr_366T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyT_Tri_136) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyT_'8869'_4 Source #

d_tri'8658'dec'8776'_426T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyT_Tri_136) → AgdaAnyAgdaAnyT_Dec_32 Source #

d_tri'8658'dec'60'_462T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyT_Tri_136) → AgdaAnyAgdaAnyT_Dec_32 Source #

d_trans'8743'tri'8658'resp'691'_498T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyT_Tri_136) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_trans'8743'tri'8658'resp'737'_582T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyT_Tri_136) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_trans'8743'tri'8658'resp_650T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyT_Tri_136) → T_Σ_14 Source #

d_wlog_682T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyT__'8846'__30) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyAgdaAny Source #

d_dec'8658'weaklyDec_734T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyT_Dec_32) → AgdaAnyAgdaAnyMaybe AgdaAny Source #

d_dec'8658'recomputable_742T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyT_Dec_32) → AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_map'45'NonEmpty_766T_Level_18 → () → T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → T_NonEmpty_316T_NonEmpty_316 Source #

d_flip'45'Connex_788T_Level_18 → () → T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyT__'8846'__30) → AgdaAnyAgdaAnyT__'8846'__30 Source #

d_subst'10230'resp'737'_796T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → ((AgdaAny → ()) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_subst'10230'resp'691'_798T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → ((AgdaAny → ()) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_subst'10230'resp'8322'_800T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → ((AgdaAny → ()) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → T_Σ_14 Source #

d_P'45'resp'10230''172'P'45'resp_802T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyAgdaAny → (AgdaAnyT_'8869'_4) → AgdaAnyT_'8869'_4 Source #

d_total'10230'refl_804T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → T_Σ_14 → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyT__'8846'__30) → AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_total'43'dec'10230'dec_806T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyT__'8846'__30) → (AgdaAnyAgdaAnyT_Dec_32) → AgdaAnyAgdaAnyT_Dec_32 Source #

d_trans'8743'irr'10230'asym_808T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyT_'8869'_4) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyT_'8869'_4 Source #

d_irr'8743'antisym'10230'asym_810T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyT_'8869'_4) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyT_'8869'_4 Source #

d_asym'10230'antisym_812T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyT_'8869'_4) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_asym'10230'irr_814T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → T_Σ_14 → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyT_'8869'_4) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyT_'8869'_4 Source #

d_tri'10230'asym_816T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyT_Tri_136) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyT_'8869'_4 Source #

d_tri'10230'irr_818T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyT_Tri_136) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyT_'8869'_4 Source #

d_tri'10230'dec'8776'_820T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyT_Tri_136) → AgdaAnyAgdaAnyT_Dec_32 Source #

d_tri'10230'dec'60'_822T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyT_Tri_136) → AgdaAnyAgdaAnyT_Dec_32 Source #

d_trans'8743'tri'10230'resp'691''8776'_824T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyT_Tri_136) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_trans'8743'tri'10230'resp'737''8776'_826T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyT_Tri_136) → AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_trans'8743'tri'10230'resp'8776'_828T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyT_Tri_136) → T_Σ_14 Source #

d_dec'10230'weaklyDec_830T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyT_Dec_32) → AgdaAnyAgdaAnyMaybe AgdaAny Source #

d_dec'10230'recomputable_832T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyT_Dec_32) → AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #