The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

Oops, if you really want to only use vm_compute it should be

Theorem refl: exists x, x=3+4.
Proof.
match goal with |- exists _, _ = ?X =>
  let y := eval vm_compute in X in
  exists y; vm_cast_no_check (refl_equal y)
end.
Qed.


On 04/22/2017 03:07 PM, Laurent Thery wrote:
> On 04/22/2017 02:55 PM, Kenneth Roe wrote:
> > Theorem refl: exists x, x=3+4.
> > Proof.
> >      apply ex_intro.
> >      (* vm_compute. *)
> >      compute.
> >      reflexivity.
> > Qed.
>
> One way to go is to match the goal
>
> Theorem refl: exists x, x=3+4.
> Proof.
> match goal with |- exists _, _ = ?X =>
>    let y := eval vm_compute in X in
>    exists y; reflexivity
> end.
> Qed.