diff options
| author | Michael Soegtrop | 2021-03-23 21:52:04 +0100 |
|---|---|---|
| committer | Michael Soegtrop | 2021-03-23 21:52:04 +0100 |
| commit | fa2ba1571cbd791c3b1acd87adeacd0aa4bd6e88 (patch) | |
| tree | 02838cbe413809dacc416d0e71102aac9f37ae1c /doc/sphinx | |
| parent | 285d5e03a230af7b327cba0b7720217ede664761 (diff) | |
| parent | aba594ca194390bb00f8ef60ef8a5eef6694fc07 (diff) | |
Merge PR #13914: Allow the presence of type casts for return values in Ltac2.
Reviewed-by: MSoegtropIMC
Reviewed-by: Zimmi48
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 9f3f0ef3d5..146da8bb37 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -263,10 +263,10 @@ There is dedicated syntax for list and array literals. .. prodn:: ltac2_expr ::= @ltac2_expr5 ; @ltac2_expr | @ltac2_expr5 - ltac2_expr5 ::= fun {+ @tac2pat0 } => @ltac2_expr + ltac2_expr5 ::= fun {+ @tac2pat0 } {? : @ltac2_type } => @ltac2_expr | let {? rec } @ltac2_let_clause {* with @ltac2_let_clause } in @ltac2_expr | @ltac2_expr3 - ltac2_let_clause ::= {+ @tac2pat0 } := @ltac2_expr + ltac2_let_clause ::= {+ @tac2pat0 } {? : @ltac2_type } := @ltac2_expr ltac2_expr3 ::= {+, @ltac2_expr2 } ltac2_expr2 ::= @ltac2_expr1 :: @ltac2_expr2 | @ltac2_expr1 @@ -304,7 +304,7 @@ Ltac2 Definitions .. insertprodn tac2def_body tac2def_body .. prodn:: - tac2def_body ::= {| _ | @ident } {* @tac2pat0 } := @ltac2_expr + tac2def_body ::= {| _ | @ident } {* @tac2pat0 } {? : @ltac2_type } := @ltac2_expr This command defines a new global Ltac2 value. If one or more :token:`tac2pat0` are specified, the new value is a function. This is a shortcut for one of the |