From f0b64a73907acc71c47d8cc76e41bb5bd7070358 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 24 Jul 2023 17:43:55 +0200
Subject: [PATCH] Comment.
---
iris/proofmode/base.v | 34 +++++++++++++++++++++++++++++-----
1 file changed, 29 insertions(+), 5 deletions(-)
diff --git a/iris/proofmode/base.v b/iris/proofmode/base.v
index 80dfe224a..6b169bdba 100644
--- a/iris/proofmode/base.v
+++ b/iris/proofmode/base.v
@@ -6,6 +6,35 @@ From Ltac2 Require Ltac2.
(** * Utility definitions used by the proofmode *)
+(** ** N-ary tactics *)
+(** Ltac1 does not provide primitives to manipulate lists (e.g., [ident_list],
+[simple_intropattern_list], needed for [iIntros], [iDestruct], etc. We can do
+that in Ltac2. For most proofmode tactics we only need to iterate over a list
+(either in forward or backward direction). The Ltac1 tactics [ltac1_list_iter]
+and [ltac1_list_rev_iter] allow us to do that while encapsulating the Ltac2
+code. These tactics can be used as:
+
+ Ltac iTactic_ xs :=
+ ltac1_list_rev_iter ltac:(fun x => /* stuff */) xs.
+ Tactic Notation "iTactic" "(" ne_ident_list(xs) ")" :=
+ iTactic_ xs.
+
+It is important to note that given one n-ary [Tactic Notation] we cannot call
+another n-ary [Tactic Notation]. For example, the following does NOT work:
+
+ Tactic Notation "iAnotherTactic" "(" ne_ident_list(xs) ")" :=
+ /* stuff */
+ iTactic (xs).
+
+Because of this reason, as already shown above, we typically provide an [Ltac]
+called [iTactic_] (note the underscore), and define the [Tactic Notation] as a
+wrapper, allowing us to write:
+
+ Tactic Notation "iAnotherTactic" "(" ne_ident_list(xs) ")" :=
+ /* stuff */
+ iTactic_ xs.
+*)
+
Ltac2 of_ltac1_list l := Option.get (Ltac1.to_list l).
Ltac ltac1_list_iter tac l :=
@@ -18,11 +47,6 @@ Ltac ltac1_list_rev_iter tac l :=
(List.rev (of_ltac1_list l))) in
go tac l.
-(* Sample use:
-Tactic Notation "foo" ident_list(xs) :=
- ltac1_list_rev_iter ltac:(fun x => intros x) xs.
-*)
-
(* Directions of rewrites *)
Inductive direction := Left | Right.
--
GitLab