Subject: Ssreflect Users Discussion List
List archive
- From: Jason Gross <>
- To: ssreflect <>
- Subject: [ssreflect] ? pattern does not work with case
- Date: Wed, 4 Jun 2014 12:11:32 +0100
In the code
Require Import ssreflect.
Goal forall x y : bool, x = y.
intros.
case ?: x => [|].
intros.
case ?: x => [|].
The [case] does not introduce an equation hypothesis. If I replace the "?" with, say, "H", then I get an equation hypothesis. Is this expected behavior?
-Jason
- [ssreflect] ? pattern does not work with case, Jason Gross, 06/04/2014
- Re: [ssreflect] ? pattern does not work with case, Enrico Tassi, 06/04/2014
Archive powered by MHonArc 2.6.18.