Module

Data.Leibniz

Package
purescript-leibniz
Repository
paf31/purescript-leibniz

This module defines a data type for Leibniz equality.

#Leibniz Source

newtype Leibniz a b

Two types are equal if they are equal in all contexts.

Constructors

Instances

#type (~) Source

Operator alias for Data.Leibniz.Leibniz (non-associative / precedence 4)

#runLeibniz Source

runLeibniz :: forall b a f. a ~ b -> f a -> f b

Unpack a Leibniz equality.

#symm Source

symm :: forall b a. a ~ b -> b ~ a

Equality is symmetric.

#coerce Source

coerce :: forall b a. a ~ b -> a -> b

Coerce a value of type a to a value of the Leibniz-equal type b.

#coerceSymm Source

coerceSymm :: forall b a. a ~ b -> b -> a

Coerce a value of type b to a value of the Leibniz-equal type a.

#liftLeibniz Source

liftLeibniz :: forall b a f. a ~ b -> (f a) ~ (f b)

Lift equality over a type constructor.

#liftLeibniz1of2 Source

liftLeibniz1of2 :: forall c b a f. a ~ b -> (f a c) ~ (f b c)

Lift equality over a type constructor.

#liftLeibniz2of2 Source

liftLeibniz2of2 :: forall c b a f. a ~ b -> (f c a) ~ (f c b)

Lift equality over a type constructor.

#liftLeibniz1of3 Source

liftLeibniz1of3 :: forall d c b a f. a ~ b -> (f a c d) ~ (f b c d)

Lift equality over a type constructor.

#liftLeibniz2of3 Source

liftLeibniz2of3 :: forall d c b a f. a ~ b -> (f c a d) ~ (f c b d)

Lift equality over a type constructor.

#liftLeibniz3of3 Source

liftLeibniz3of3 :: forall d c b a f. a ~ b -> (f c d a) ~ (f c d b)

Lift equality over a type constructor.

#lowerLeibniz Source

lowerLeibniz :: forall b a f. (f a) ~ (f b) -> a ~ b

Every type constructor in PureScript is injective.

#lowerLeibniz1of2 Source

lowerLeibniz1of2 :: forall d c b a f. (f a c) ~ (f b d) -> a ~ b

Every type constructor in PureScript is injective.

#lowerLeibniz2of2 Source

lowerLeibniz2of2 :: forall d c b a f. (f a c) ~ (f b d) -> c ~ d

Every type constructor in PureScript is injective.

#lowerLeibniz1of3 Source

lowerLeibniz1of3 :: forall g e d c b a f. (f a b c) ~ (f d e g) -> a ~ d

Every type constructor in PureScript is injective.

#lowerLeibniz2of3 Source

lowerLeibniz2of3 :: forall g e d c b a f. (f a b c) ~ (f d e g) -> b ~ e

Every type constructor in PureScript is injective.

#lowerLeibniz3of3 Source

lowerLeibniz3of3 :: forall g e d c b a f. (f a b c) ~ (f d e g) -> c ~ g

Every type constructor in PureScript is injective.

Modules
Data.Leibniz