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

MAlonzo.Code.Data.Product.Relation.Binary.Pointwise.NonDependent

Documentation

d_Pointwise_40T_Level_18 → () → T_Level_18 → () → T_Level_18T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → T_Σ_14T_Σ_14 → () Source #

d_'215''45'reflexive_54T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → T_Σ_14T_Σ_14T_Σ_14T_Σ_14 Source #

d_'215''45'refl_60T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → T_Σ_14T_Σ_14 Source #

d_'215''45'irreflexive'8321'_66T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyT_Irrelevant_20) → T_Σ_14T_Σ_14T_Σ_14T_Σ_14T_Irrelevant_20 Source #

d_'215''45'irreflexive'8322'_74T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyT_Irrelevant_20) → T_Σ_14T_Σ_14T_Σ_14T_Σ_14T_Irrelevant_20 Source #

d_'215''45'symmetric_82T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → T_Σ_14T_Σ_14T_Σ_14T_Σ_14 Source #

d_'215''45'transitive_88T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → T_Σ_14T_Σ_14T_Σ_14T_Σ_14T_Σ_14T_Σ_14 Source #

d_'215''45'antisymmetric_94T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → T_Σ_14T_Σ_14T_Σ_14T_Σ_14T_Σ_14 Source #

d_'215''45'respects'691'_116T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → T_Σ_14T_Σ_14T_Σ_14T_Σ_14T_Σ_14T_Σ_14 Source #

d_'215''45'respects'737'_122T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → T_Σ_14T_Σ_14T_Σ_14T_Σ_14T_Σ_14T_Σ_14 Source #

d_'215''45'respects'8322'_128T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Σ_14T_Σ_14T_Σ_14 Source #

d_'215''45'total_130T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyT__'8846'__30) → (AgdaAnyAgdaAnyT__'8846'__30) → T_Σ_14T_Σ_14T__'8846'__30 Source #

d_'215''45'decidable_222T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyT_Dec_20) → (AgdaAnyAgdaAnyT_Dec_20) → T_Σ_14T_Σ_14T_Dec_20 Source #

d_'215''45'isPreorder_260T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_Level_18 → (AgdaAnyAgdaAny → ()) → T_IsPreorder_70T_IsPreorder_70T_IsPreorder_70 Source #