Stefan Holdermans wrote:
Daniel,
Interestingly, we can also use induction to reason about infinite list.
To this end, we use _|_ (`bottom' or `undefined') as a base case.
To prove something for both finite and infinite lists, one uses two base
cases (_|_, and []) and takes the inductive step.
Are you sure this makes sense for a lazy language?
Conor
--
http://www.cs.nott.ac.uk/~ctm
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe