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

MAlonzo.Code.Relation.Binary.Lattice

Documentation

d_Supremum_12T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_Infimum_30T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_Exponential_40T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_IsJoinSemilattice_68 ∷ p → p → p → p → p → p → p → () Source #

d_'8744''45'least_122T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → T_IsJoinSemilattice_68AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_refl_140T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → T_IsJoinSemilattice_68AgdaAnyAgdaAny Source #

d_JoinSemilattice_170 ∷ p → p → p → () Source #

d_IsBoundedJoinSemilattice_262 ∷ p → p → p → p → p → p → p → p → () Source #

d_refl_298T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsBoundedJoinSemilattice_262AgdaAnyAgdaAny Source #

d_BoundedJoinSemilattice_336 ∷ p → p → p → () Source #

d_IsMeetSemilattice_438 ∷ p → p → p → p → p → p → p → () Source #

d_refl_510T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → T_IsMeetSemilattice_438AgdaAnyAgdaAny Source #

d_MeetSemilattice_540 ∷ p → p → p → () Source #

d_IsBoundedMeetSemilattice_632 ∷ p → p → p → p → p → p → p → p → () Source #

d_refl_670T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsBoundedMeetSemilattice_632AgdaAnyAgdaAny Source #

d_BoundedMeetSemilattice_706 ∷ p → p → p → () Source #

d_IsLattice_810 ∷ p → p → p → p → p → p → p → p → () Source #

d_x'8804'x'8744'y_846T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → T_IsLattice_810AgdaAnyAgdaAnyAgdaAny Source #

d_y'8804'x'8744'y_848T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → T_IsLattice_810AgdaAnyAgdaAnyAgdaAny Source #

d_'8744''45'least_850T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → T_IsLattice_810AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_x'8743'y'8804'x_854T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → T_IsLattice_810AgdaAnyAgdaAnyAgdaAny Source #

d_x'8743'y'8804'y_856T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → T_IsLattice_810AgdaAnyAgdaAnyAgdaAny Source #

d_'8743''45'greatest_858T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → T_IsLattice_810AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_refl_868T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → T_IsLattice_810AgdaAnyAgdaAny Source #

d_'8764''45'resp'45''8776'_874T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → T_IsLattice_810T_Σ_14 Source #

d_reflexive_886T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → T_IsLattice_810AgdaAnyAgdaAnyT__'8801'__12AgdaAny Source #

d_Lattice_898 ∷ p → p → p → () Source #

d_IsDistributiveLattice_1012 ∷ p → p → p → p → p → p → p → p → () Source #

d_refl_1054T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → T_IsDistributiveLattice_1012AgdaAnyAgdaAny Source #

d_DistributiveLattice_1098 ∷ p → p → p → () Source #

d_IsBoundedLattice_1226 ∷ p → p → p → p → p → p → p → p → p → p → () Source #

d_refl_1276T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsBoundedLattice_1226AgdaAnyAgdaAny Source #

d_x'8743'y'8804'x_1284T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsBoundedLattice_1226AgdaAnyAgdaAnyAgdaAny Source #

d_x'8743'y'8804'y_1286T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsBoundedLattice_1226AgdaAnyAgdaAnyAgdaAny Source #

d_x'8804'x'8744'y_1288T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsBoundedLattice_1226AgdaAnyAgdaAnyAgdaAny Source #

d_y'8804'x'8744'y_1290T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsBoundedLattice_1226AgdaAnyAgdaAnyAgdaAny Source #

d_'8743''45'greatest_1292T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsBoundedLattice_1226AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_'8744''45'least_1294T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsBoundedLattice_1226AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_reflexive_1308T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsBoundedLattice_1226AgdaAnyAgdaAnyT__'8801'__12AgdaAny Source #

d_BoundedLattice_1324 ∷ p → p → p → () Source #

d_IsHeytingAlgebra_1468 ∷ p → p → p → p → p → p → p → p → p → p → p → () Source #

d_transpose'45''8680'_1506T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsHeytingAlgebra_1468AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_transpose'45''8743'_1522T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsHeytingAlgebra_1468AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_refl_1558T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsHeytingAlgebra_1468AgdaAnyAgdaAny Source #

d_x'8743'y'8804'x_1566T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsHeytingAlgebra_1468AgdaAnyAgdaAnyAgdaAny Source #

d_x'8743'y'8804'y_1568T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsHeytingAlgebra_1468AgdaAnyAgdaAnyAgdaAny Source #

d_x'8804'x'8744'y_1570T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsHeytingAlgebra_1468AgdaAnyAgdaAnyAgdaAny Source #

d_y'8804'x'8744'y_1572T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsHeytingAlgebra_1468AgdaAnyAgdaAnyAgdaAny Source #

d_'8743''45'greatest_1574T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsHeytingAlgebra_1468AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_'8744''45'least_1576T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsHeytingAlgebra_1468AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_reflexive_1590T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsHeytingAlgebra_1468AgdaAnyAgdaAnyT__'8801'__12AgdaAny Source #

d_HeytingAlgebra_1602 ∷ p → p → p → () Source #

d_IsBooleanAlgebra_1760 ∷ p → p → p → p → p → p → p → p → p → p → p → () Source #

d__'8680'__1792T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsBooleanAlgebra_1760AgdaAnyAgdaAnyAgdaAny Source #

d_refl_1830T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsBooleanAlgebra_1760AgdaAnyAgdaAny Source #

d_transpose'45''8680'_1838T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsBooleanAlgebra_1760AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_transpose'45''8743'_1840T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsBooleanAlgebra_1760AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_x'8743'y'8804'x_1842T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsBooleanAlgebra_1760AgdaAnyAgdaAnyAgdaAny Source #

d_x'8743'y'8804'y_1844T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsBooleanAlgebra_1760AgdaAnyAgdaAnyAgdaAny Source #

d_x'8804'x'8744'y_1846T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsBooleanAlgebra_1760AgdaAnyAgdaAnyAgdaAny Source #

d_y'8804'x'8744'y_1848T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsBooleanAlgebra_1760AgdaAnyAgdaAnyAgdaAny Source #

d_'8743''45'greatest_1850T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsBooleanAlgebra_1760AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_'8744''45'least_1852T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsBooleanAlgebra_1760AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_reflexive_1866T_Level_18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsBooleanAlgebra_1760AgdaAnyAgdaAnyT__'8801'__12AgdaAny Source #

d_BooleanAlgebra_1878 ∷ p → p → p → () Source #