0 | module Data.Fun.Graph
 1 |
 2 | ||| A relation corresponding to the graph of `f`.
 3 | public export
 4 | record Graph {0 a : Type} {0 b : a -> Type}
 5 |              (f : (x : a) -> b x) (x : a) (y : b x) where
 6 |   constructor MkGraph
 7 |   equality : f x === y
 8 |
 9 | ||| An alternative for 'Syntax.WithProof' that allows to keep the
10 | ||| proof certificate in non-reduced form after nested matching.
11 | ||| Inspired by https://agda.github.io/agda-stdlib/README.Inspect.html
12 | public export
13 | remember : {0 a : Type} -> {0 b : a -> Type} ->
14 |            (f : (x : a) -> b x) -> (x : a) -> Graph f x (f x)
15 | remember _ _ = MkGraph Refl
16 |