coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Embedding tactics inside terms?

From: Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Embedding tactics inside terms?
Date: Tue, 7 Apr 2020 12:07:17 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=agnishom AT cmi.ac.in; spf=Pass smtp.mailfrom=agnishom AT cmi.ac.in; spf=None smtp.helo=postmaster AT mail.cmi.ac.in
Ironport-phdr: 9a23:uN5XkxxlNtTDHhfXCy+O+j09IxM/srCxBDY+r6Qd2+seIJqq85mqBkHD//Il1AaPAdyGrasZwLOO7eigATVGvc/d9ihaMdRlbFwst4Y/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVImbuv6FZTPgMupyuu854PcYxlShDq6fLh+MAi6oR/eu8ULgYZuMLs9xxvGrndVZ+hbxH5jKVaPkxrh/Mu984Nv/itKt/4968JMVLjxcrglQ7BfEDkpPGc56dHxuxLeVwWP/HwcUmsXkhpMHQfI6QzxU4nyvCXnqOdzwTGWMsLqQ786XzSi9LprRwTziCgbLT458XrYhdJ2galGvR+uvR1/w4rTYIGIKPpze77WcN0GSWZdWMtaSipMCZ6+YYQSFeoMJelXr4f/qFUOoxWwBhSiCv3zxTJTnHD6wbc33v49HQ3a3gEtGc8FvnTOrNXyMacfSfy4zKbOzTXCdPNW2TD96I3VeR0/ofGDR65wcdbWyUk3DQzKk1WQqIz/MDKVy+8AtHKU7+VmVeKukG4nqwZxoj20y8gwj4nJh5gZxUrY+iljwYY1I8S1RUhmatCqF5tQsjuVN4pwQs46QmFovjw6yrwctpKhcigK0pIqzAPcZfyfa4WE/w/vWeaLLTtmi39oe6iziwiv/US61+HxVdW43E5UoiZZltTArHMA2hzJ5sSaS/Zw/12t1DmR2w3V9+pKO1o7lbDBJJ4k2rMwloQcsUDEHiLunUX5lq6WdkE+9ue07uTnY6/qqYWAOINuiwH+NLwims25AesmLggDR3WX9fm82bH540H0T7ZHguconqXEqpzWOMcWqrKhDw9QyIkj6hK/Dzm80NQfmHkKNEhKeB2Bj4joIFHOIPf4DfKkjluwlTdrxurKMaf9DZnXL3jDlq/tfaxh5E5E1Aoz0ddf6opIBbEGOfL/Q1P+tNjFDhAiKAG02ObmCNBl1owEQ26PA6mZMLnTsVCS/O4vLfOMN8cpv2P2LOFg7Przh1c4n0UcdO+nx8g5cne9S91pJUSCYX3pyvwBGHsWuRI3QOz7gUzKBTdcYXepX6U5zjo+CcSvBsHCQNb+0/S6wC6nE8gONSh9AVeWHCKwLtnWa7I3cCuXZ/RZvHkcT7H4Et0q0BDovQS8yrw1drOJqB1djorq0Z1O38OWlRw28mUqXcGU0mXLRGR12GoDAT4wjvgm8B5Nj2yb2K09uMR2UNla5vdHSAA/bMeOxOl7Tdn5HAPHLI6E

Perfect. This is what I was looking for.

On Tue, Apr 7, 2020 at 12:02 PM Alix Trieu <alix.trieu AT cs.au.dk> wrote:

Hi,

There is “ltac:()” command as described here https://coq.inria.fr/refman/language/gallina-extensions.html?highlight=ltac#solving-existential-variables-using-tactics

For instance, you could write ltac:(auto) where a term would be expected.

Alix

On 7 Apr 2020, at 18:58, Agnishom Chattopadhyay <agnishom AT cmi.ac.in> wrote:

Hi;

Lean has a feature that allows them to use a (begin ... end) block enclosing a tactic anywhere a term is expected. Do we have some similar feature in Coq?

--Agnishom

[Coq-Club] Embedding tactics inside terms?, Agnishom Chattopadhyay, 04/07/2020
- Re: [Coq-Club] Embedding tactics inside terms?, Alix Trieu, 04/07/2020
  - Re: [Coq-Club] Embedding tactics inside terms?, Agnishom Chattopadhyay, 04/07/2020