| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Nullary.Reflects
Documentation
d_Reflects_16 ∷ p → p → p → () Source #
data T_Reflects_16 Source #
Constructors
| C_of'696'_22 AgdaAny | |
| C_of'8319'_26 |
d_of_30 ∷ T_Level_18 → () → Bool → AgdaAny → T_Reflects_16 Source #
d_invert_38 ∷ T_Level_18 → () → Bool → T_Reflects_16 → AgdaAny Source #
d_recompute_46 ∷ T_Level_18 → () → Bool → T_Reflects_16 → AgdaAny → AgdaAny Source #
d_recompute'45'constant_62 ∷ T_Level_18 → () → Bool → T_Reflects_16 → AgdaAny → AgdaAny → T__'8801'__12 Source #
d_'172''45'reflects_70 ∷ T_Level_18 → () → Bool → T_Reflects_16 → T_Reflects_16 Source #
d__'215''45'reflects__82 ∷ T_Level_18 → () → T_Level_18 → () → Bool → Bool → T_Reflects_16 → T_Reflects_16 → T_Reflects_16 Source #
d__'8846''45'reflects__98 ∷ T_Level_18 → () → T_Level_18 → () → Bool → Bool → T_Reflects_16 → T_Reflects_16 → T_Reflects_16 Source #
d__'8594''45'reflects__114 ∷ T_Level_18 → () → T_Level_18 → () → Bool → Bool → T_Reflects_16 → T_Reflects_16 → T_Reflects_16 Source #
d_fromEquivalence_132 ∷ T_Level_18 → () → Bool → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Reflects_16 Source #
du_fromEquivalence_132 ∷ Bool → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Reflects_16 Source #
d_det_146 ∷ T_Level_18 → () → Bool → Bool → T_Reflects_16 → T_Reflects_16 → T__'8801'__12 Source #