Idris2Doc : Libraries.Decidable.Equality

Libraries.Decidable.Equality

(source)
Reexports
import public Decidable.Equality
Definitions
maybeEq : DecEq a => (x : a) -> (y : a) -> Maybe (x = y)
  Visibility: public export
maybeCong : (f : (a -> b)) -> Maybe (x = y) -> Maybe (f x = f y)
  Visibility: public export
maybeCong2 : (f : (a -> b -> c)) -> Maybe (x = y) -> Maybe (v = w) -> Maybe (f x v = f y w)
  Visibility: public export