diff options
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 15 | ||||
| -rw-r--r-- | test-suite/ltac2/rebind.v | 25 |
2 files changed, 31 insertions, 9 deletions
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. diff --git a/test-suite/ltac2/rebind.v b/test-suite/ltac2/rebind.v index 6cec49de1e..86c755363e 100644 --- a/test-suite/ltac2/rebind.v +++ b/test-suite/ltac2/rebind.v @@ -35,16 +35,31 @@ Ltac2 Set g := f. (* Rebinding with old values *) -Ltac2 mutable qux () := Message.print (Message.of_string "Hello"). +Ltac2 Type rec nat := [O | S (nat)]. -Ltac2 Set qux as self := fun () => self (); self (). +Ltac2 rec nat_eq n m := + match n with + | O => match m with | O => true | S _ => false end + | S n => match m with | O => false | S m => nat_eq n m end + end. -Ltac2 Eval qux (). +Ltac2 Type exn ::= [ Assertion_failed ]. + +Ltac2 assert_eq n m := + match nat_eq n m with + | true => () + | false => Control.throw Assertion_failed end. + + +Ltac2 mutable qux n := S n. + +Ltac2 Set qux as self := fun n => self (self n). + +Ltac2 Eval assert_eq (qux O) (S (S O)). -Ltac2 Type rec nat := [O | S (nat)]. Ltac2 mutable quz := O. Ltac2 Set quz as self := S self. -Ltac2 Eval quz. +Ltac2 Eval (assert_eq quz (S O)). |