# Documentation

Lazyness properties of `Nat`

makes it ideal for lazy list length computation.
Examples:

length [1..] > 100

length undefined >= 0

length (undefined: undefined) >= 1

Rank computation with lazy Peano numbers.

The dependence function represents a graph with multiedges (edges with multiple start nodes).
`dependence n`

is the list of the start nodes of all multiedges whose end node is `n`

.

`nodeRank n`

computes the length of the shortest path to `n`

. Note that if `n`

is an end point of a multiedge with no start point,
then `nodeRank n == 0`

.

- If
`any null (dependence n)`

then`nodeRank n == 0`

. - Otherwise
`nodeRank n == 1 + minimum [maximum (map nodeRank l1), maximum (map nodeRank l2), ..] where`

[l1, l2, ..] == dependence n`if this is computable.`

- Otherwise the rank is
`infinity`

. (These cases are observable.)

:: (n -> [[n]]) | dependence function |

-> (n -> Nat) | memoised version of the result function |

-> n -> Nat | rank of a node |

Memoising version of `nodeRank`

.

The rank of inaccessable nodes are `inductive_infinity`

.
These cases are observable with the predicate `(> n)`

where `n`

is an upper bound for the number of nodes in the graph.

`nodeRankMemo`

specialised for integral types.