The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

This seems to work:

Definition SC_aux{T}(a:T) : Prop.
exact True.
Qed.

Ltac simply_convertible x y :=
  let d := constr:(ltac:(clear; intro; assumption):(SC_aux x -> SC_aux 
y)) in idtac.


-- Jonathan


On 10/30/2016 05:59 PM, Jonathan Leivent wrote:
> That would work for top-level evars, but it would be harder to do if 
> there are evars under binders.
>
> --Jonathan
>
> On 10/30/2016 05:21 PM, Jason Gross wrote:
> > You can assert the goal [term1 = term2], generalize over all of the 
> > evars,
> > and then see if [reflexivity] solves your goal.  Is this what you're
> > looking for?
> >
> > On Sun, Oct 30, 2016 at 4:38 PM Jonathan Leivent 
> > <jonikelee AT gmail.com>
> > wrote:
> >
> > > Is there any way in Ltac to test if two terms are convertible without
> > > inducing any evar instantiation, and without doing unnecessary 
> > > reduction?
> > >
> > >
> > > -- Jonathan