Idris2Doc : Control.Function

Control.Function

Definitions

interfaceInjective : (a->b) ->Type
  An injective function maps distinct elements to distinct elements.

Parameters: f
Constructor: MkInjective
Methods:
injective : fx=fy->x=y

Implementations:
InjectiveJust
InjectiveS
InjectiveFS
InjectivefinToNat
injective : Injectivef=>fx=fy->x=y
Visibility: public export
inj : (0f : (a->b)) -> {auto0_ : Injectivef} -> (0_ : fx=fy) ->x=y
Visibility: public export