Lists from functions #
Theorems and lemmas for dealing with
list.of_fn, which converts a function on
fin n to a list
Main Definitions #
The main definitions pertain to lists generated using
The length of a list converted from a function is the size of the domain.
nth element of a list
Arrays converted to lists are the same as
of_fn on the indexing function of the array.
of_fn on an empty domain is the empty list.