coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] evar-aware destruct?
- Date: Thu, 20 Nov 2014 22:35:35 -0500
Hi,
Is there any way to destruct a variable in a way that results in the fresh hypotheses being accessible from an evar? I would like something like the following to work:
Ltac evar1_aware_destruct_nat n :=
instantiate (1 := match n with 0 => _ | _ => _ end);
let n' := fresh "n'" in
destruct n as [|n'].
Goal forall n : nat, exists n0, match n with 0 => 0 | S n' => S n' end = n0.
Proof.
intros.
eexists.
evar1_aware_destruct_nat n; [ reflexivity | ].
instantiate (1 := n'). (* Error: Instance is not well-typed in the environment of ?589 *)
Thanks,
Jason
- [Coq-Club] evar-aware destruct?, Jason Gross, 11/21/2014
- Re: [Coq-Club] evar-aware destruct?, Guillaume Melquiond, 11/21/2014
Archive powered by MHonArc 2.6.18.