From e559dfc4995ae6777d9ff07d34db738cb77a519c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 4 Feb 2020 18:40:24 +0100 Subject: Adding an alias "pose proof (x:=a)" for "pose proof a as x". This is to be consistent with "pose (x:=a)" (and an alternative to "assert (x:=a)"). This was suggested by "https://github.com/HoTT/HoTT/pull/1208#discussion_r374342962". --- .../04-tactics/11522-master+pose-proof-wo-as-syntax.rst | 6 ++++++ doc/sphinx/proof-engine/tactics.rst | 13 +++++++++++++ 2 files changed, 19 insertions(+) create mode 100644 doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst (limited to 'doc') diff --git a/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst b/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst new file mode 100644 index 0000000000..579ccf839f --- /dev/null +++ b/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst @@ -0,0 +1,6 @@ +- **Added:** + Syntax :tacn:`pose proof (@ident:=@term)` as an + alternative to `pose proof @term as @ident`, following the model of + :tacn:`pose (@ident:=@term)` + (`#11522 `_, + by Hugo Herbelin). diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 6a0ce20c79..206342fef1 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1452,6 +1452,19 @@ Controlling the proof flow While :tacn:`pose proof` expects that no existential variables are generated by the tactic, :tacn:`epose proof` removes this constraint. +.. tacv:: pose proof (@ident := @term) + + This is an alternative syntax for :n:`assert (@ident := @term)` and + :n:`pose proof @term as @ident`, following the model of :n:`pose + (@ident := @term)` but dropping the value of :token:`ident`. + +.. tacv:: epose proof (@ident := @term) + + This is an alternative syntax for :n:`eassert (@ident := @term)` + and :n:`epose proof @term as @ident`, following the model of + :n:`epose (@ident := @term)` but dropping the value of + :token:`ident`. + .. tacv:: enough (@ident : @type) :name: enough -- cgit v1.2.3 From 7c1733040a19846359cdf7725b20c93398b50d3b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 3 Mar 2020 14:20:14 +0100 Subject: Update doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst Co-Authored-By: Théo Zimmermann --- doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'doc') diff --git a/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst b/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst index 579ccf839f..3dd103b115 100644 --- a/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst +++ b/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst @@ -1,6 +1,6 @@ - **Added:** - Syntax :tacn:`pose proof (@ident:=@term)` as an - alternative to `pose proof @term as @ident`, following the model of - :tacn:`pose (@ident:=@term)` + Syntax :n:`pose proof (@ident:=@term)` as an + alternative to :n:`pose proof @term as @ident`, following the model of + :n:`pose (@ident:=@term)`. See documentation of :tacn:`pose proof` (`#11522 `_, by Hugo Herbelin). -- cgit v1.2.3