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

MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise

Documentation

d_Pointwise_70 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_Pointwise_70 #

Constructors

C_inj'8321'_88 AgdaAny 
C_inj'8322'_94 AgdaAny 

d_map_100 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 #

du_map_100 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 #

d_drop'45'inj'8321'_114 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> T_Pointwise_70 -> AgdaAny #

du_drop'45'inj'8321'_114 :: T_Pointwise_70 -> AgdaAny #

d_drop'45'inj'8322'_122 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> T_Pointwise_70 -> AgdaAny #

du_drop'45'inj'8322'_122 :: T_Pointwise_70 -> AgdaAny #

d_'8846''45'refl_126 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T_Pointwise_70 #

du_'8846''45'refl_126 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T_Pointwise_70 #

d_'8846''45'symmetric_140 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 #

du_'8846''45'symmetric_140 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 #

d_'8846''45'transitive_154 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 -> T_Pointwise_70 #

du_'8846''45'transitive_154 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 -> T_Pointwise_70 #

d_'8846''45'asymmetric_172 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20) -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 -> T_Irrelevant_20 #

d_'46'extendedlambda0_180 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20) -> AgdaAny -> AgdaAny -> AgdaAny -> T_Pointwise_70 -> T_Irrelevant_20 #

d_'46'extendedlambda1_190 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20) -> AgdaAny -> AgdaAny -> AgdaAny -> T_Pointwise_70 -> T_Irrelevant_20 #

d_'8846''45'substitutive_194 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> ((AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> ((AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (T__'8846'__30 -> ()) -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> AgdaAny -> AgdaAny #

du_'8846''45'substitutive_194 :: ((AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> ((AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (T__'8846'__30 -> ()) -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> AgdaAny -> AgdaAny #

d_'8846''45'decidable_212 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T_Dec_20) -> (AgdaAny -> AgdaAny -> T_Dec_20) -> T__'8846'__30 -> T__'8846'__30 -> T_Dec_20 #

du_'8846''45'decidable_212 :: (AgdaAny -> AgdaAny -> T_Dec_20) -> (AgdaAny -> AgdaAny -> T_Dec_20) -> T__'8846'__30 -> T__'8846'__30 -> T_Dec_20 #

d_'8846''45'reflexive_246 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 #

du_'8846''45'reflexive_246 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 #

d_'8846''45'irreflexive_260 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20) -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 -> T_Irrelevant_20 #

d_'8846''45'antisymmetric_278 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 -> T_Pointwise_70 #

du_'8846''45'antisymmetric_278 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 -> T_Pointwise_70 #

d_'8846''45'respects'737'_296 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 -> T_Pointwise_70 #

du_'8846''45'respects'737'_296 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 -> T_Pointwise_70 #

d_'8846''45'respects'691'_314 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 -> T_Pointwise_70 #

du_'8846''45'respects'691'_314 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 -> T_Pointwise_70 #

d_'8846''45'respects'8322'_332 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14 #

du_'8846''45'respects'8322'_332 :: T_Σ_14 -> T_Σ_14 -> T_Σ_14 #

d_'8846''45'isEquivalence_342 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsEquivalence_26 #

du_'8846''45'isEquivalence_342 :: T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsEquivalence_26 #

d_'8846''45'isDecEquivalence_352 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecEquivalence_44 -> T_IsDecEquivalence_44 -> T_IsDecEquivalence_44 #

du_'8846''45'isDecEquivalence_352 :: T_IsDecEquivalence_44 -> T_IsDecEquivalence_44 -> T_IsDecEquivalence_44 #

d_'8846''45'isPreorder_362 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPreorder_70 -> T_IsPreorder_70 -> T_IsPreorder_70 #

du_'8846''45'isPreorder_362 :: T_IsPreorder_70 -> T_IsPreorder_70 -> T_IsPreorder_70 #

d_'8846''45'isPartialOrder_372 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPartialOrder_174 -> T_IsPartialOrder_174 -> T_IsPartialOrder_174 #

du_'8846''45'isPartialOrder_372 :: T_IsPartialOrder_174 -> T_IsPartialOrder_174 -> T_IsPartialOrder_174 #

d_'8846''45'isStrictPartialOrder_382 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290 #

du_'8846''45'isStrictPartialOrder_382 :: T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290 #

d_'8846''45'setoid_392 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44 #

du_'8846''45'setoid_392 :: T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44 #

d_'8846''45'decSetoid_402 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DecSetoid_84 -> T_DecSetoid_84 -> T_DecSetoid_84 #

du_'8846''45'decSetoid_402 :: T_DecSetoid_84 -> T_DecSetoid_84 -> T_DecSetoid_84 #

d_'8846''45'preorder_412 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Preorder_132 -> T_Preorder_132 -> T_Preorder_132 #

du_'8846''45'preorder_412 :: T_Preorder_132 -> T_Preorder_132 -> T_Preorder_132 #

d_'8846''45'poset_422 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Poset_314 -> T_Poset_314 -> T_Poset_314 #

du_'8846''45'poset_422 :: T_Poset_314 -> T_Poset_314 -> T_Poset_314 #

d__'8846''8347'__432 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44 #

du__'8846''8347'__432 :: T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44 #

d_Pointwise'45''8801''8658''8801'_434 :: T_Level_18 -> () -> T_Level_18 -> () -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T__'8801'__12 #

d_'8801''8658'Pointwise'45''8801'_440 :: T_Level_18 -> () -> T_Level_18 -> () -> T__'8846'__30 -> T__'8846'__30 -> T__'8801'__12 -> T_Pointwise_70 #

du_'8801''8658'Pointwise'45''8801'_440 :: T__'8846'__30 -> T_Pointwise_70 #

d_Pointwise'45''8801''8596''8801'_446 :: T_Level_18 -> T_Level_18 -> () -> () -> T_Inverse_1960 #

du_Pointwise'45''8801''8596''8801'_446 :: T_Inverse_1960 #