Idris2Doc : Data.Fun.Graph

Data.Fun.Graph

recordGraph : {0 b : a -> Type} -> ((x : a) -> bx) -> (x : a) -> bx -> Type
  A relation corresponding to the graph of `f`.

Totality: total
Constructor: 
MkGraph : fx = y -> Graphfxy

Projection: 
.equality : Graphfxy -> fx = y
remember : {0 b : a -> Type} -> (f : ((x : a) -> bx)) -> (x : a) -> Graphfx (fx)
  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