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

MAlonzo.Code.Relation.Unary.Properties

Documentation

d_'8838''45'reflexive_62T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14AgdaAnyAgdaAnyAgdaAny Source #

d_'8838''45'trans_68T_Level_18 → () → T_Level_18T_Level_18T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyAgdaAny Source #

d_'8838''45'antisym_76T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → T_Σ_14 Source #

d_'8834''8658''8838'_82T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14AgdaAnyAgdaAnyAgdaAny Source #

d_'8834''45'trans_84T_Level_18 → () → T_Level_18T_Level_18T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14T_Σ_14T_Σ_14 Source #

d_'8834''45''8838''45'trans_100T_Level_18 → () → T_Level_18T_Level_18T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → (AgdaAnyAgdaAnyAgdaAny) → T_Σ_14 Source #

d_'8838''45''8834''45'trans_114T_Level_18 → () → T_Level_18T_Level_18T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → T_Σ_14T_Σ_14 Source #

d_'8834''45'resp'691''45''8784'_128T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14T_Σ_14T_Σ_14 Source #

d_'8834''45'resp'737''45''8784'_134T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14T_Σ_14T_Σ_14 Source #

d_'8834''45'antisym_148T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14T_Σ_14T_Σ_14 Source #

d_'8834''45'asym_154T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14T_Σ_14T_Irrelevant_20 Source #

d_'8838''8242''45'trans_178T_Level_18 → () → T_Level_18T_Level_18T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyAgdaAny Source #

d_'8838''8242''45'antisym_188T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → T_Σ_14 Source #

d_'8834''8242''45'trans_196T_Level_18 → () → T_Level_18T_Level_18T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14T_Σ_14T_Σ_14 Source #

d_'8834''8242''45''8838''8242''45'trans_208T_Level_18 → () → T_Level_18T_Level_18T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14 → (AgdaAnyAgdaAnyAgdaAny) → T_Σ_14 Source #

d_'8838''8242''45''8834''8242''45'trans_218T_Level_18 → () → T_Level_18T_Level_18T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → T_Σ_14T_Σ_14 Source #

d_'8834''8242''45'antisym_248T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14T_Σ_14T_Σ_14 Source #

d_'8838''8658''8838''8242'_254T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyAgdaAny Source #

d_'8838''8242''8658''8838'_260T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyAgdaAny Source #

d_'8784''45'sym_276T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14T_Σ_14 Source #

d_'8784''45'trans_278T_Level_18 → () → T_Level_18T_Level_18T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14T_Σ_14T_Σ_14 Source #

d_'8784''8242''45'sym_298T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14T_Σ_14 Source #

d_'8784''8242''45'trans_300T_Level_18 → () → T_Level_18T_Level_18T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → T_Σ_14T_Σ_14T_Σ_14 Source #

d_'8705''63'_324T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAnyT_Dec_20) → AgdaAnyT_Dec_20 Source #

d__'8746''63'__334T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAnyT_Dec_20) → (AgdaAnyT_Dec_20) → AgdaAnyT_Dec_20 Source #

d__'8745''63'__346T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAnyT_Dec_20) → (AgdaAnyT_Dec_20) → AgdaAnyT_Dec_20 Source #

d__'215''63'__358T_Level_18 → () → T_Level_18T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAnyT_Dec_20) → (AgdaAnyT_Dec_20) → T_Σ_14T_Dec_20 Source #

d__'8857''63'__372T_Level_18 → () → T_Level_18T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAnyT_Dec_20) → (AgdaAnyT_Dec_20) → T_Σ_14T_Dec_20 Source #

d__'8846''63'__386T_Level_18 → () → T_Level_18T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAnyT_Dec_20) → (AgdaAnyT_Dec_20) → T__'8846'__30T_Dec_20 Source #

d__'126''63'_402T_Level_18 → () → T_Level_18 → () → T_Level_18 → (T_Σ_14 → ()) → (T_Σ_14T_Dec_20) → T_Σ_14T_Dec_20 Source #