| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.Construct.Add.Extrema.Strict
Documentation
d__'60''8331'__22 ∷ p → p → p → p → p → p → () Source #
d__'60''8314'__82 ∷ p → p → p → p → p → p → () Source #
d_'91''60''93''45'injective_158 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T__'60''8314'__20 → AgdaAny Source #
d_'60''177''45'asym_160 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'60''8314'__20 → T__'60''8314'__20 → T_'8869'_4 Source #
d_'60''177''45'trans_162 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'60''8314'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #
du_'60''177''45'trans_162 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'60''8314'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #
d_'60''177''45'dec_164 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T_Dec_32 Source #
du_'60''177''45'dec_164 ∷ (AgdaAny → AgdaAny → T_Dec_32) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T_Dec_32 Source #
d_'60''177''45'irrelevant_166 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'60''8314'__20 → T__'60''8314'__20 → T__'8801'__12 Source #
d__'8804''8314'__178 ∷ p → p → p → p → p → p → p → p → () Source #
d_'60''177''45'trans'691'_232 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8804''8314'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #
du_'60''177''45'trans'691'_232 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8804''8314'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #
d_'60''177''45'trans'737'_234 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'60''8314'__20 → T__'8804''8314'__20 → T__'60''8314'__20 Source #
du_'60''177''45'trans'737'_234 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'60''8314'__20 → T__'8804''8314'__20 → T__'60''8314'__20 Source #
d_'60''177''45'cmp'45''8801'_236 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Tri_136) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T_Tri_136 Source #
du_'60''177''45'cmp'45''8801'_236 ∷ (AgdaAny → AgdaAny → T_Tri_136) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T_Tri_136 Source #
d_'60''177''45'irrefl'45''8801'_238 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → T_'8869'_4) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8801'__12 → T__'60''8314'__20 → T_'8869'_4 Source #
d_'60''177''45'resp'737''45''8801'_240 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8801'__12 → T__'60''8314'__20 → T__'60''8314'__20 Source #
d_'60''177''45'resp'691''45''8801'_242 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8801'__12 → T__'60''8314'__20 → T__'60''8314'__20 Source #
d_'60''177''45'resp'45''8801'_244 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Σ_14 Source #
d__'8776''8729'__256 ∷ p → p → p → p → p → p → p → p → () Source #
d_'60''177''45'cmp_282 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Tri_136) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T_Tri_136 Source #
du_'60''177''45'cmp_282 ∷ (AgdaAny → AgdaAny → T_Tri_136) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T_Tri_136 Source #
d_'60''177''45'irrefl_284 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 → T__'60''8314'__20 → T_'8869'_4 Source #
d_'60''177''45'resp'737''45''8776''177'_286 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #
du_'60''177''45'resp'737''45''8776''177'_286 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #
d_'60''177''45'resp'691''45''8776''177'_288 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #
du_'60''177''45'resp'691''45''8776''177'_288 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → Maybe (Maybe AgdaAny) → T__'8776''8729'__20 → T__'60''8314'__20 → T__'60''8314'__20 Source #
d_'60''177''45'resp'45''8776''177'_290 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Σ_14 → T_Σ_14 Source #
d_'60''177''45'isStrictPartialOrder'45''8801'_292 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_266 → T_IsStrictPartialOrder_266 Source #
du_'60''177''45'isStrictPartialOrder'45''8801'_292 ∷ T_IsStrictPartialOrder_266 → T_IsStrictPartialOrder_266 Source #
d_'60''177''45'isDecStrictPartialOrder'45''8801'_294 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_314 → T_IsDecStrictPartialOrder_314 Source #
du_'60''177''45'isDecStrictPartialOrder'45''8801'_294 ∷ T_IsDecStrictPartialOrder_314 → T_IsDecStrictPartialOrder_314 Source #
d_'60''177''45'isStrictTotalOrder'45''8801'_296 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → T_IsStrictTotalOrder_502 Source #
du_'60''177''45'isStrictTotalOrder'45''8801'_296 ∷ T_IsStrictTotalOrder_502 → T_IsStrictTotalOrder_502 Source #
d__'8776''8729'__308 ∷ p → p → p → p → p → p → p → p → () Source #
d_'60''177''45'isStrictPartialOrder_334 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_266 → T_IsStrictPartialOrder_266 Source #
du_'60''177''45'isStrictPartialOrder_334 ∷ T_IsStrictPartialOrder_266 → T_IsStrictPartialOrder_266 Source #
d_'60''177''45'isDecStrictPartialOrder_336 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecStrictPartialOrder_314 → T_IsDecStrictPartialOrder_314 Source #
du_'60''177''45'isDecStrictPartialOrder_336 ∷ T_IsDecStrictPartialOrder_314 → T_IsDecStrictPartialOrder_314 Source #
d_'60''177''45'isStrictTotalOrder_338 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → T_IsStrictTotalOrder_502 Source #