The Coq mailing list

[Jean-Christophe Filliatre <filliatr AT lri.fr>]

satrajit AT attbi.com
 writes:
 > I'm new to Coq. Here's what I need to do:
 > 
 > Definition A:B->B:=
 >     [b:B] Cases b of
 >          (foo b') => ......
 >          _        => _
 >     end.
 > 
 > However, I'm getting the following error at the last but one line:
 > Error: The reference _ was not found in the current environment.
 > 
 > I assume, the construct _ => _, which I noticed in a similar
 > definition in a  
 > paper based on Coq V6.10, is no longer supported. What is the way
 > out? 

You should write instead:

  Definition A:B->B:=
      [b:B] Cases b of
           (foo b') => ......
           x        => x

Indeed, "_"  on the left side  is a pattern  (matching everything) but
"_" on the right side is seen as a variable, thus unbound.

Best regards,
-- 
Jean-Christophe Filliâtre