From 457cee4345ab4ad6b6624a6886841fd0b0739b2a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 30 Jan 2020 08:18:49 +0100 Subject: Allow to rebind the old value of a mutable Ltac2 entry. --- doc/sphinx/proof-engine/ltac2.rst | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'doc/sphinx/proof-engine') diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 35062e0057..0eb7ac6bb2 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -226,12 +226,14 @@ Ltac Definitions If ``mutable`` is set, the definition can be redefined at a later stage (see below). -.. cmd:: Ltac2 Set @qualid := @ltac2_term +.. cmd:: Ltac2 Set @qualid {? as @lident} := @ltac2_term :name: Ltac2 Set This command redefines a previous ``mutable`` definition. Mutable definitions act like dynamic binding, i.e. at runtime, the last defined value for this entry is chosen. This is useful for global flags and the like. + The previous value of the binding can be optionally accessed using the `as` + binding syntax. Reduction ~~~~~~~~~ -- cgit v1.2.3 From 6cb24494fe8b6e945c6b6696134a6a42ecdab6ec Mon Sep 17 00:00:00 2001 From: Kenji Maillard Date: Sun, 10 May 2020 15:14:42 +0200 Subject: Correcting ltac2's documentation on values turning test into proper check. --- doc/sphinx/proof-engine/ltac2.rst | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) (limited to 'doc/sphinx/proof-engine') diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 0eb7ac6bb2..2ec1d0521e 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -213,14 +213,21 @@ There is dedicated syntax for list and array literals. Ltac Definitions ~~~~~~~~~~~~~~~~ -.. cmd:: Ltac2 {? mutable} {? rec} @lident := @ltac2_term +.. cmd:: Ltac2 {? mutable} {? rec} @lident := @ltac2_value :name: Ltac2 This command defines a new global Ltac2 value. - For semantic reasons, the body of the Ltac2 definition must be a syntactical - value, that is, a function, a constant or a pure constructor recursively applied to - values. + The body of an Ltac2 definition is required to be a syntactical value + that is, a function, a constant, a pure constructor recursively applied to + values or a (non-recursive) let binding of a value in a value. + + .. productionlist:: coq + ltac2_value: fun `ltac2_var` => `ltac2_term` + : `ltac2_qualid` + : `ltac2_constructor` `ltac2_value` ... `ltac2_value` + : `ltac2_var` + : let `ltac2_var` := `ltac2_value` in `ltac2_value` If ``rec`` is set, the tactic is expanded into a recursive binding. -- cgit v1.2.3 From 639b19e04b7e9ccad109d3c4a0149b65ed8287fe Mon Sep 17 00:00:00 2001 From: Kenji Maillard Date: Tue, 12 May 2020 12:06:58 +0200 Subject: documenting with examples the dynamic behaviour of Ltac2 Set --- doc/sphinx/proof-engine/ltac2.rst | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) (limited to 'doc/sphinx/proof-engine') diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 2ec1d0521e..1e35160205 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -242,6 +242,35 @@ Ltac Definitions The previous value of the binding can be optionally accessed using the `as` binding syntax. + .. example:: Dynamic nature of mutable cells + + .. coqtop:: all + + Ltac2 mutable x := true. + Ltac2 y := x. + Ltac2 Eval y. + Ltac2 Set x := false. + Ltac2 Eval y. + + .. example:: Interaction with recursive calls + + + .. coqtop:: all + + Ltac2 mutable rec f b := match b with true => 0 | _ => f true end. + Ltac2 Set f := fun b => + match b with true => 1 | _ => f true end. + Ltac2 Eval (f false). + Ltac2 Set f as oldf := fun b => + match b with true => 2 | _ => oldf false end. + Ltac2 Eval (f false). + + In the definition, the `f` in the body is resolved statically + because the definition is marked recursive. In the first re-definition, + the `f` in the body is resolved dynamically. This is witnessed by + the second re-definition. + + Reduction ~~~~~~~~~ -- cgit v1.2.3