Data.Fun.Graph

Definitions

record Graph : {0 b : a -> Type} -> ((x : a) -> b x) -> (x : a) -> b x -> Type

  A relation corresponding to the graph of `f`.

Totality: total
Visibility: public export
Constructor: 

MkGraph : f x = y -> Graph f x y

Projection: 

.equality : Graph f x y -> f x = y

.equality : Graph f x y -> f x = y

Visibility: public export

equality : Graph f x y -> f x = y

Visibility: public export

remember : {0 b : a -> Type} -> (f : ((x : a) -> b x)) -> (x : a) -> Graph f x (f x)

  An alternative for 'Syntax.WithProof' that allows to keep the
  proof certificate in non-reduced form after nested matching.
  Inspired by https://agda.github.io/agda-stdlib/README.Inspect.html

Visibility: public export