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

MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict

Documentation

d__'60''8314'__20 :: p -> p -> p -> p -> p -> p -> () #

data T__'60''8314'__20 #

Constructors

C_'91'_'93'_26 AgdaAny 
C_'91'_'93''60''8868''8314'_30 

d_'91''60''93''45'injective_36 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> T__'60''8314'__20 -> AgdaAny #

du_'91''60''93''45'injective_36 :: T__'60''8314'__20 -> AgdaAny #

d_'60''8314''45'asym_40 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20) -> Maybe AgdaAny -> Maybe AgdaAny -> T__'60''8314'__20 -> T__'60''8314'__20 -> T_Irrelevant_20 #

d_'60''8314''45'trans_48 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny -> T__'60''8314'__20 -> T__'60''8314'__20 -> T__'60''8314'__20 #

du_'60''8314''45'trans_48 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny -> T__'60''8314'__20 -> T__'60''8314'__20 -> T__'60''8314'__20 #

d_'60''8314''45'dec_62 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T_Dec_20) -> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_20 #

du_'60''8314''45'dec_62 :: (AgdaAny -> AgdaAny -> T_Dec_20) -> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_20 #

d_'60''8314''45'irrelevant_80 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12) -> Maybe AgdaAny -> Maybe AgdaAny -> T__'60''8314'__20 -> T__'60''8314'__20 -> T__'8801'__12 #

d__'8804''8314'__102 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

d_'60''8314''45'trans'691'_154 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8804''8314'__20 -> T__'60''8314'__20 -> T__'60''8314'__20 #

du_'60''8314''45'trans'691'_154 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8804''8314'__20 -> T__'60''8314'__20 -> T__'60''8314'__20 #

d_'60''8314''45'trans'737'_168 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny -> T__'60''8314'__20 -> T__'8804''8314'__20 -> T__'60''8314'__20 #

du_'60''8314''45'trans'737'_168 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny -> T__'60''8314'__20 -> T__'8804''8314'__20 -> T__'60''8314'__20 #

d_'60''8314''45'cmp'45''8801'_184 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T_Tri_158) -> Maybe AgdaAny -> Maybe AgdaAny -> T_Tri_158 #

du_'60''8314''45'cmp'45''8801'_184 :: (AgdaAny -> AgdaAny -> T_Tri_158) -> Maybe AgdaAny -> Maybe AgdaAny -> T_Tri_158 #

d_'60''8314''45'irrefl'45''8801'_240 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> T_Irrelevant_20) -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8801'__12 -> T__'60''8314'__20 -> T_Irrelevant_20 #

d_'60''8314''45'resp'737''45''8801'_246 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8801'__12 -> T__'60''8314'__20 -> T__'60''8314'__20 #

du_'60''8314''45'resp'737''45''8801'_246 :: T__'60''8314'__20 -> T__'60''8314'__20 #

d_'60''8314''45'resp'691''45''8801'_250 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8801'__12 -> T__'60''8314'__20 -> T__'60''8314'__20 #

du_'60''8314''45'resp'691''45''8801'_250 :: T__'60''8314'__20 -> T__'60''8314'__20 #

d_'60''8314''45'resp'45''8801'_254 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 #

du_'60''8314''45'resp'45''8801'_254 :: T_Σ_14 #

d__'8776''8729'__266 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

d_'60''8314''45'cmp_296 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T_Tri_158) -> Maybe AgdaAny -> Maybe AgdaAny -> T_Tri_158 #

du_'60''8314''45'cmp_296 :: (AgdaAny -> AgdaAny -> T_Tri_158) -> Maybe AgdaAny -> Maybe AgdaAny -> T_Tri_158 #

d_'60''8314''45'irrefl_354 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20) -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8776''8729'__20 -> T__'60''8314'__20 -> T_Irrelevant_20 #

d_'60''8314''45'resp'737''45''8776''8314'_362 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8776''8729'__20 -> T__'60''8314'__20 -> T__'60''8314'__20 #

du_'60''8314''45'resp'737''45''8776''8314'_362 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8776''8729'__20 -> T__'60''8314'__20 -> T__'60''8314'__20 #

d_'60''8314''45'resp'691''45''8776''8314'_380 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8776''8729'__20 -> T__'60''8314'__20 -> T__'60''8314'__20 #

du_'60''8314''45'resp'691''45''8776''8314'_380 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8776''8729'__20 -> T__'60''8314'__20 -> T__'60''8314'__20 #

d_'60''8314''45'resp'45''8776''8314'_392 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 #

du_'60''8314''45'resp'45''8776''8314'_392 :: T_Σ_14 -> T_Σ_14 #

d_'60''8314''45'isStrictPartialOrder'45''8801'_394 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290 #

du_'60''8314''45'isStrictPartialOrder'45''8801'_394 :: T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290 #

d_'60''8314''45'isDecStrictPartialOrder'45''8801'_430 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_336 -> T_IsDecStrictPartialOrder_336 #

du_'60''8314''45'isDecStrictPartialOrder'45''8801'_430 :: T_IsDecStrictPartialOrder_336 -> T_IsDecStrictPartialOrder_336 #

d_'60''8314''45'isStrictTotalOrder'45''8801'_478 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_534 -> T_IsStrictTotalOrder_534 #

du_'60''8314''45'isStrictTotalOrder'45''8801'_478 :: T_IsStrictTotalOrder_534 -> T_IsStrictTotalOrder_534 #

d__'8776''8729'__542 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

d_'60''8314''45'isStrictPartialOrder_572 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290 #

du_'60''8314''45'isStrictPartialOrder_572 :: T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290 #

d_'60''8314''45'isDecStrictPartialOrder_608 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_336 -> T_IsDecStrictPartialOrder_336 #

du_'60''8314''45'isDecStrictPartialOrder_608 :: T_IsDecStrictPartialOrder_336 -> T_IsDecStrictPartialOrder_336 #

d_'60''8314''45'isStrictTotalOrder_656 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_534 -> T_IsStrictTotalOrder_534 #

du_'60''8314''45'isStrictTotalOrder_656 :: T_IsStrictTotalOrder_534 -> T_IsStrictTotalOrder_534 #