Idris2Doc : Control.Function

Control.Function

interface Injective : (a -> b) -> Type
  Parameters: f
Constructor: MkInjective
Methods:
  
injective : f x = f y -> x = y

Implementations:
  
Injective (\{arg:0} => x ::: arg)
  
Injective (\{arg:0} => arg ::: ys)
  
Injective Just
  
Injective S
  
Injective FS
  
Injective finToNat
inj : (0 f : (a -> b)) -> {auto 0 _ : Injective f} -> (0 _ : f x = f y) -> x = y
  
injective : Injective f => f x = f y -> x = y