Idris2Doc : Data.Fun.Graph

Data.Fun.Graph

Definitions

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

Totality: total
Visibility: public export
Constructor: 
MkGraph : fx=y->Graphfxy

Projection: 
.equality : Graphfxy->fx=y
.equality : Graphfxy->fx=y
Visibility: public export
equality : Graphfxy->fx=y
Visibility: public export
remember : {0b : 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

Visibility: public export