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_28T_Level_18T_Level_18T_Level_18T_Level_18 → () → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → T_Σ_14T_Σ_14 → () Source #

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

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

d_'215''45'irreflexive'8321'_70T_Level_18T_Level_18T_Level_18T_Level_18 → () → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyT_'8869'_4) → T_Σ_14T_Σ_14T_Σ_14T_Σ_14T_'8869'_4 Source #

d_'215''45'irreflexive'8322'_86T_Level_18T_Level_18T_Level_18T_Level_18 → () → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyT_'8869'_4) → T_Σ_14T_Σ_14T_Σ_14T_Σ_14T_'8869'_4 Source #

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

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

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

d_'215''45'asymmetric'8321'_148T_Level_18T_Level_18T_Level_18T_Level_18 → () → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyT_'8869'_4) → T_Σ_14T_Σ_14T_Σ_14T_Σ_14T_'8869'_4 Source #

d_'215''45'asymmetric'8322'_160T_Level_18T_Level_18T_Level_18T_Level_18 → () → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyT_'8869'_4) → T_Σ_14T_Σ_14T_Σ_14T_Σ_14T_'8869'_4 Source #

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

d__'8764'__194T_Level_18T_Level_18T_Level_18T_Level_18 → () → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → T_Σ_14T_Σ_14T_Σ_14T_Σ_14 → () Source #

d__'8776'__196T_Level_18T_Level_18T_Level_18T_Level_18 → () → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → T_Σ_14T_Σ_14T_Σ_14T_Σ_14 → () Source #

d_resp'185'_202T_Level_18T_Level_18T_Level_18T_Level_18 → () → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → T_Σ_14T_Σ_14T_Σ_14T_Σ_14T_Σ_14T_Σ_14T_Σ_14T_Σ_14 Source #

d_resp'178'_212T_Level_18T_Level_18T_Level_18T_Level_18 → () → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → T_Σ_14T_Σ_14T_Σ_14T_Σ_14T_Σ_14T_Σ_14T_Σ_14T_Σ_14 Source #

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

d_'215''45'decidable_318T_Level_18T_Level_18T_Level_18T_Level_18 → () → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyT_Dec_32) → (AgdaAnyAgdaAnyT_Dec_32) → T_Σ_14T_Σ_14T_Dec_32 Source #

d_'215''45'isPreorder_372T_Level_18T_Level_18T_Level_18T_Level_18 → () → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → T_IsPreorder_70T_IsPreorder_70T_IsPreorder_70 Source #

d__'215''45'Rel__518T_Level_18T_Level_18T_Level_18T_Level_18 → () → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → T_Σ_14T_Σ_14 → () Source #

d__'215''45'reflexive__522T_Level_18T_Level_18T_Level_18T_Level_18 → () → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → T_Σ_14T_Σ_14T_Σ_14T_Σ_14 Source #

d__'215''45'refl__524T_Level_18T_Level_18T_Level_18T_Level_18 → () → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → T_Σ_14T_Σ_14 Source #

d__'215''45'symmetric__526T_Level_18T_Level_18T_Level_18T_Level_18 → () → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAny) → T_Σ_14T_Σ_14T_Σ_14T_Σ_14 Source #

d__'215''45'transitive__528T_Level_18T_Level_18T_Level_18T_Level_18 → () → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → T_Σ_14T_Σ_14T_Σ_14T_Σ_14T_Σ_14T_Σ_14 Source #

d__'215''45'antisymmetric__530T_Level_18T_Level_18T_Level_18T_Level_18 → () → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → T_Σ_14T_Σ_14T_Σ_14T_Σ_14T_Σ_14 Source #

d__'215''45''8776''45'respects'8322'__532T_Level_18T_Level_18T_Level_18T_Level_18 → () → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → T_Σ_14T_Σ_14T_Σ_14 Source #

d__'215''45'decidable__534T_Level_18T_Level_18T_Level_18T_Level_18 → () → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyT_Dec_32) → (AgdaAnyAgdaAnyT_Dec_32) → T_Σ_14T_Σ_14T_Dec_32 Source #

d__'215''45'isPreorder__540T_Level_18T_Level_18T_Level_18T_Level_18 → () → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → T_IsPreorder_70T_IsPreorder_70T_IsPreorder_70 Source #

d__'215''45''8799'__556T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAnyAgdaAnyT_Dec_32) → (AgdaAnyAgdaAnyAgdaAnyT_Dec_32) → T_Σ_14T_Σ_14T_Dec_32 Source #