The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 05/01/2021 22:36, jonikelee AT gmail.com wrote:
> Does Ltac2 yet have the ability to modify something defined at
> top-level from within a tactic?  I can't seem to even define a
> top-level Ltac2 definition with a mutable type.  For instance (in
> 8.12.1), I get an error trying to do the following:

Not being able to define arbitrary terms as Ltac2 entry points is a
voluntary limitation of the Ltac2 runtime that is due to considerations
about Coq document structures (including but not limited to backtrack
and evaluation across several processes).

As you guessed, you can currently only modify an Ltac2 mutable
definition through a vernacular command. That said, it's in my TODO list
to extend this ability to runtime with a dynamic setter, e.g. something
along the lines of

let mutable mydef := foo in tac

where mydef will be set to foo inside tac. I have to first decide
whether I want to stick to a state-like (i.e. global) or a reader-like
(i.e. well-scoped dynamic binding) behaviour first, but apart from that
it's not very hard to implement.

PMP

Attachment: OpenPGP_signature
Description: OpenPGP digital signature