diff options
| author | Pierre-Marie Pédrot | 2020-10-21 14:41:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-04 17:53:02 +0100 |
| commit | 2559f0474c8cd66b5020524d1e758ea7a19bc8fb (patch) | |
| tree | f18d993b9dcfd9a4c816befa8cf1e7cbaa7858bf | |
| parent | f661944a302a024f1120212c21c093a7dae67642 (diff) | |
Document the syntax addition.
| -rw-r--r-- | doc/changelog/05-tactic-language/13232-ltac2-if-then-else.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 17 |
2 files changed, 16 insertions, 6 deletions
diff --git a/doc/changelog/05-tactic-language/13232-ltac2-if-then-else.rst b/doc/changelog/05-tactic-language/13232-ltac2-if-then-else.rst new file mode 100644 index 0000000000..d105561a23 --- /dev/null +++ b/doc/changelog/05-tactic-language/13232-ltac2-if-then-else.rst @@ -0,0 +1,5 @@ +- **Added:** + An if-then-else syntax to Ltac2 + (`#13232 <https://github.com/coq/coq/pull/13232>`_, + fixes `#10110 <https://github.com/coq/coq/issues/10110>`_, + by Pierre-Marie Pédrot). diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 64fc1133f0..d4e49dda5b 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -38,7 +38,6 @@ Current limitations include: - Printing functions are limited and awkward to use. Only a few data types are printable. - Deep pattern matching and matching on tuples don't work. - - If statements on Ltac2 boolean values - A convenient way to build terms with casts through the low-level API. Because the cast type is opaque, building terms with casts currently requires an awkward construction like the following, which also incurs extra overhead to repeat typechecking for each @@ -267,6 +266,7 @@ There is dedicated syntax for list and array literals. | @ltac2_expr5 ltac2_expr5 ::= fun {+ @tac2pat0 } => @ltac2_expr | let {? rec } @ltac2_let_clause {* with @ltac2_let_clause } in @ltac2_expr + | if @ltac2_expr5 then @ltac2_expr5 else @ltac2_expr5 | @ltac2_expr3 ltac2_let_clause ::= {+ @tac2pat0 } := @ltac2_expr ltac2_expr3 ::= {+, @ltac2_expr2 } @@ -345,12 +345,10 @@ Ltac2 Definitions .. 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 mutable rec f b := if b then 0 else f true. + Ltac2 Set f := fun b => if b then 1 else f true. Ltac2 Eval (f false). - Ltac2 Set f as oldf := fun b => - match b with true => 2 | _ => oldf false end. + Ltac2 Set f as oldf := fun b => if b then 2 else oldf false. Ltac2 Eval (f false). In the definition, the `f` in the body is resolved statically @@ -1149,6 +1147,13 @@ Match on values | @tac2pat1 , {*, @tac2pat1 } | @tac2pat1 +.. tacn:: if @ltac2_expr5__test then @ltac2_expr5__then else @ltac2_expr5__else + :name: if-then-else (Ltac2) + + Equivalent to a :tacn:`match <match (Ltac2)>` on a boolean value. If the + :n:`@ltac2_expr5__test` evaluates to true, :n:`@ltac2_expr5__then` + is evaluated. Otherwise :n:`@ltac2_expr5__else` is evaluated. + .. note:: For now, deep pattern matching is not implemented. |