The Coq mailing list

[Jean Goubault-Larrecq <goubault AT lsv.ens-cachan.fr>]

satrajit AT attbi.com
 wrote:
> I'm new to Coq. Here's what I need to do:
>
> Definition A:B->B:=
>     [b:B] Cases b of
>          (foo b') => ......
>          _        => _
>     end.

        You forgot the pipe sign;
write:
        | _ => etc.



        -- Jean Goubault-Larrecq, LSV, tel:+33-1 47 40 75 68.