The Coq mailing list

[Brandon Moore <brandon_m_moore AT yahoo.com>]

> From: Stéphane Lescuyer 
>Â <stephane.lescuyer AT inria.fr>

> 
> ...
> 
> The other thing I would be worried about is '_' patterns,  where
> writing something like:
> 
> match c1, c2 with
> | TAB, CR =>  true
> | _, _ => false
> end
> 
> would look harmless while actually  expanding to a 256*256 matching tree.

A minor point, but I think that expands to a 256+256 matching tree.
I would expect all but the TAB branch of the outer match to not
decompose the second argument. It seems that's how it actually
works, at least with a smaller example. Perhaps something with dependent
types might see the pathological case.

Example:

Inductive foo : Set := A | B | C | D | E .

Definition bar : foo -> foo -> bool := fun x y =>
  match x, y with
  | A, B => true
  | _, _ => false
  end.

Print bar.

produces

bar = 
fun x y : foo =>
match x with
| A =>
    match y with
    | A => false
    | B => true
    | C => false
    | D => false
    | E => false
    end
| B => false
| C => false
| D => false
| E => false
end
     : foo -> foo -> bool