Idris2Doc : Control.Function

Control.Function

interfaceInjective : (a -> b) -> Type
Parameters: f
Constructor: MkInjective
Methods:
injective : fx = fy -> x = y

Implementations:
Injective (\{arg:0} => x:::arg)
Injective (\{arg:0} => arg:::ys)
InjectiveJust
InjectiveS
InjectiveFS
InjectivefinToNat
inj : (0 f : (a -> b)) -> {auto 0 _ : Injectivef} -> (0 _ : fx = fy) -> x = y
injective : Injectivef => fx = fy -> x = y