[Haskell-cafe] bottom case in proof by induction
Martijn van Steenbergen
martijn at van.steenbergen.nl
Wed Dec 31 20:16:39 EST 2008
Luke Palmer wrote:
> First, by simple definition, id _|_ = _|_. Now let's consider foo _|_.
> The Haskell semantics say that pattern matching on _|_ yields _|_, so
> foo _|_ = _|_. So they are equivalent on _|_ also. Thus foo and id are
> exactly the same function.
Would it in general also be interesting to look at foo == id for input
(_|_:xs) and all other possible positions and combinations of positions
for bottom? I wonder how many cases you need to take into consideration
to have covered every possible situation.
More information about the Haskell-Cafe