| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Nullary.Decidable
Documentation
d_map_18 ∷ T_Level_18 → () → T_Level_18 → () → T_Equivalence_1714 → T_Dec_20 → T_Dec_20 Source #
d__'8776'__114 ∷ T_GeneralizeTel_1875 → T_Setoid_44 → T_Setoid_44 → T_Injection_776 → AgdaAny → AgdaAny → () Source #
d__'8776'__138 ∷ T_GeneralizeTel_1875 → T_Setoid_44 → T_Setoid_44 → T_Injection_776 → AgdaAny → AgdaAny → () Source #
d_via'45'injection_160 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_776 → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_Dec_20 Source #
du_via'45'injection_160 ∷ T_Injection_776 → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_Dec_20 Source #
d_True'45''8596'_238 ∷ T_Level_18 → () → T_Dec_20 → (AgdaAny → AgdaAny → T__'8801'__12) → T_Inverse_1960 Source #
d_isYes'8791'does_256 ∷ T_Level_18 → () → T_Dec_20 → T__'8801'__12 Source #
d_dec'45'true_260 ∷ T_Level_18 → () → T_Dec_20 → AgdaAny → T__'8801'__12 Source #
d_dec'45'false_270 ∷ T_Level_18 → () → T_Dec_20 → (AgdaAny → T_Irrelevant_20) → T__'8801'__12 Source #
d_dec'45'yes_282 ∷ T_Level_18 → () → T_Dec_20 → AgdaAny → T_Σ_14 Source #
d_dec'45'no_298 ∷ T_Level_18 → () → T_Dec_20 → (AgdaAny → T_Irrelevant_20) → T__'8801'__12 Source #
d_dec'45'yes'45'irr_312 ∷ T_Level_18 → () → T_Dec_20 → (AgdaAny → AgdaAny → T__'8801'__12) → AgdaAny → T__'8801'__12 Source #
d_'8970''8971''45'map'8242'_338 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Dec_20 → T__'8801'__12 Source #
d_GeneralizeTel_1875 ∷ () Source #
data T_GeneralizeTel_1875 Source #
Constructors
| C_mkGeneralizeTel_1877 T_Level_18 T_Level_18 T_Level_18 T_Level_18 |