coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Julien Tesson <julien.tesson AT lacl.fr>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Making tactic that return a value
- Date: Wed, 21 Oct 2015 12:33:48 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=julien.tesson AT lacl.fr; spf=None smtp.mailfrom=julien.tesson AT lacl.fr; spf=None smtp.helo=postmaster AT ns.lacl.fr
- Ironport-phdr: 9a23:eVjzGR0KD+Ti0PUZsmDT+DRfVm0co7zxezQtwd8ZsegVIvad9pjvdHbS+e9qxAeQG96LtrQc0aGN6+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6PyZztnLvqs7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGCmS4noRVC0qnwFTBA6NuBPnWpb8tG3mu/Fm3y+yOcT9SfY6Q2LxvO9QVBb0hXJfZHYC+2bNh5kogQ==
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
- [Coq-Club] Making tactic that return a value, Julien Tesson, 10/21/2015
- Re: [Coq-Club] Making tactic that return a value, Pierre Courtieu, 10/21/2015
- Re: [Coq-Club] Making tactic that return a value, Jacques-Henri Jourdan, 10/21/2015
Archive powered by MHonArc 2.6.18.