[Haskell-cafe] Clarification on proof section of HS: The Craft
of FP
Conor McBride
ctm at cs.nott.ac.uk
Mon May 2 12:57:03 EDT 2005
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
More information about the Haskell-Cafe
mailing list