The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

Hi,

One solution might be to bind the return value to some value in the
environment before returning.

-- 
JH

Le 21/10/2015 12:33, Julien Tesson a écrit :
> Hi all !
> I am currently trying to make some tactics that return values, to be used 
> by other tactics, but I have some trouble to mix this "functional style" 
> with the usual "imperative style".
> I'd like to write tactics that first do some operations on the environment 
> and then return a term like this one :
>
> Ltac test_return :=
>  let H := True in
>   assert (H=True) by reflexivity;
>   constr:H.
>
> Coq lets me define such Ltac function, but then, when I try to use it, like 
> this :
>
> Ltac  mem mem_arg :=
>       let H := fresh "Mem" in
>       pose (H := mem_arg)
>     .
>
> mem ltac:(test_return).  
>
> I get the error : "Variable mem_arg should be bound to a term". It makes me 
> think that no value is returned by the tactic called.
>
> The only workaround I found was to use a "continuation passing style" like 
> this :
>
> Ltac test_cont  cont :=
>  let H := True in
>   assert (H=True) by reflexivity;
>   cont constr:H.
>
> test_return mem.
>
> But I find this style less convenient to use.
>
> So here are my questions :
> Is there something that can make test_return work as I expected ?
> If not, I'm curious to know why such kind of thing is not permitted ?
>
> -- Julien
>

Attachment: signature.asc
Description: OpenPGP digital signature