| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Nullary.Decidable
Documentation
d_map_18 ∷ T_Level_18 → () → T_Level_18 → () → T_Equivalence_1858 → T_Dec_20 → T_Dec_20 Source #
d__'8776'__130 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → AgdaAny → AgdaAny → () Source #
d__'8776'__156 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → AgdaAny → AgdaAny → () Source #
d_via'45'injection_180 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_Dec_20 Source #
du_via'45'injection_180 ∷ T_Injection_842 → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_Dec_20 Source #
d_True'45''8596'_190 ∷ T_Level_18 → () → T_Dec_20 → (AgdaAny → AgdaAny → T__'8801'__12) → T_Inverse_2122 Source #
d_to_200 ∷ T_Level_18 → () → T_Dec_20 → (AgdaAny → AgdaAny → T__'8801'__12) → AgdaAny → AgdaAny Source #
d_from_202 ∷ T_Level_18 → () → T_Dec_20 → (AgdaAny → AgdaAny → T__'8801'__12) → AgdaAny → AgdaAny Source #
d_to'45'from_206 ∷ T_Level_18 → () → T_Dec_20 → (AgdaAny → AgdaAny → T__'8801'__12) → AgdaAny → T__'8801'__12 Source #
d_from'45'to_214 ∷ T_Level_18 → () → T_Dec_20 → (AgdaAny → AgdaAny → T__'8801'__12) → T_Dec_20 → AgdaAny → T__'8801'__12 Source #
d_isYes'8791'does_218 ∷ T_Level_18 → () → T_Dec_20 → T__'8801'__12 Source #
d_dec'45'true_222 ∷ T_Level_18 → () → T_Dec_20 → AgdaAny → T__'8801'__12 Source #
d_dec'45'false_232 ∷ T_Level_18 → () → T_Dec_20 → (AgdaAny → T_Irrelevant_20) → T__'8801'__12 Source #
d_dec'45'yes'45'recompute_244 ∷ T_Level_18 → () → T_Dec_20 → AgdaAny → T__'8801'__12 Source #
d_dec'45'yes'45'irr_258 ∷ T_Level_18 → () → T_Dec_20 → (AgdaAny → AgdaAny → T__'8801'__12) → AgdaAny → T__'8801'__12 Source #
d_dec'45'yes_270 ∷ T_Level_18 → () → T_Dec_20 → AgdaAny → T_Σ_14 Source #
d_dec'45'no_280 ∷ T_Level_18 → () → T_Dec_20 → (AgdaAny → T_Irrelevant_20) → T__'8801'__12 Source #
d_'8970''8971''45'map'8242'_296 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Dec_20 → T__'8801'__12 Source #
d_does'45''8801'_308 ∷ T_Level_18 → () → T_Dec_20 → T_Dec_20 → T__'8801'__12 Source #
d_does'45''8660'_322 ∷ T_Level_18 → () → T_Level_18 → () → T_Equivalence_1858 → T_Dec_20 → T_Dec_20 → T__'8801'__12 Source #