| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Function.Consequences.Propositional
Documentation
d_contraInjective_16 :: T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12) -> AgdaAny -> AgdaAny -> (T__'8801'__12 -> T_Irrelevant_20) -> T__'8801'__12 -> T_Irrelevant_20 #
d_inverse'691''8658'injective_18 :: T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12) -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 #
d_inverse'691''8658'strictlyInverse'691'_20 :: T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12) -> AgdaAny -> T__'8801'__12 #
d_inverse'737''8658'strictlyInverse'737'_22 :: T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12) -> AgdaAny -> T__'8801'__12 #
d_inverse'737''8658'surjective_24 :: T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12) -> AgdaAny -> T_Σ_14 #
du_inverse'737''8658'surjective_24 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12) -> AgdaAny -> T_Σ_14 #
d_inverse'7495''8658'bijective_26 :: T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 #
du_inverse'7495''8658'bijective_26 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 #
d_surjective'8658'strictlySurjective_34 :: T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T_Σ_14) -> AgdaAny -> T_Σ_14 #
du_surjective'8658'strictlySurjective_34 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> T_Σ_14) -> AgdaAny -> T_Σ_14 #
d_strictlySurjective'8658'surjective_40 :: T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T_Σ_14) -> AgdaAny -> T_Σ_14 #
du_strictlySurjective'8658'surjective_40 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> T_Σ_14) -> AgdaAny -> T_Σ_14 #
d_strictlyInverse'737''8658'inverse'737'_44 :: T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T__'8801'__12) -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 #
d_strictlyInverse'691''8658'inverse'691'_50 :: T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T__'8801'__12) -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 #