The Coq mailing list

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

> On 22 Sep 2016, at 10:27, Robbert Krebbers 
> <mailinglists AT robbertkrebbers.nl>
>  wrote:
> 
> On 09/22/2016 10:15 AM, Frédéric Besson wrote:
>>> 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.
> Jason's trick can be simplified as follows:
> 
>  Ltac is_var_bool x :=
>    constr:(ltac:(first [is_var x; exact true|exact false])).
I like this much more. This looks more like something that I can comprehend — 
the reasoning is local and at first look the efficiency seems reasonable.
This might not be king-fu tough you just need to be a little contortionist.

> 
> I sometimes use this constr:(ltac:t) trick to define tactics that return a 
> term while being implemented using possibly side-effecting tactics.
> 
> IMHO my solution isn't very pretty either...