The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

> On 21 Sep 2016, at 21:39, Jason Gross 
> <jasongross9 AT gmail.com>
>  wrote:
> 
> > In the same vein, I would be glad if a tactic such as ‘is_var' would not 
> > be a tactic but a function returning a boolean.
> 
> Ltac is_var_bool x := tryif is_var x then constr:(true) else constr:(false).
> 
> Does that work?
Doesn’t it trigger the infamous error message "expecting a tactic got a term"

>  Otherwise:
> 
> Class is_var_bool {T} (x : T) := decide_is_var : bool.
> Hint Extern 0 (is_var_bool ?x) => first [ is_var x; exact true | exact 
> false ] : typeclass_instances.
> Ltac is_var_bool x := constr:(_ : is_var_bool x).
This is what I would call Ltac kung-fu. 
A dark art which I sincerely admire but do not intend to practice. 
Remember that at OCaml level [is_var] is just a trivial pattern-matching over 
the constr i.e O(1) for a tiny 1.

Best,
—
Frédéric