From c2c74ba9c2c0d6b7e76cc4a84331000e3dd6ed85 Mon Sep 17 00:00:00 2001 From: Jacob Salzberg Date: Thu, 17 Oct 2024 11:59:04 -0400 Subject: [PATCH 1/2] Update later.v "forall quantify," to my untrained eye, looks so _wrong_ because I'm used to "forall" being a preposition and "universally" being an adverb. Does this change in the iris world? --- exercises/later.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/exercises/later.v b/exercises/later.v index 3957199..a5cac13 100644 --- a/exercises/later.v +++ b/exercises/later.v @@ -184,7 +184,7 @@ Proof. (** The tactic for Löb induction, [iLöb], requires us to specify the name of the induction hypothesis, which we here call ["IH"]. - Optionally, it can also forall quantify any of our variables before + Optionally, it can also universally quantify any of our variables before performing induction. We here forall quantify [x] as it changes for every recursive call. *) From 8479c1fa148430dff34cd3d497de98a63c727f29 Mon Sep 17 00:00:00 2001 From: Simon Gregersen Date: Fri, 8 Nov 2024 19:04:45 -0500 Subject: [PATCH 2/2] swap 'forall' for 'universally' --- exercises/later.v | 4 ++-- theories/later.v | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/exercises/later.v b/exercises/later.v index a5cac13..0d85dda 100644 --- a/exercises/later.v +++ b/exercises/later.v @@ -184,8 +184,8 @@ Proof. (** The tactic for Löb induction, [iLöb], requires us to specify the name of the induction hypothesis, which we here call ["IH"]. - Optionally, it can also universally quantify any of our variables before - performing induction. We here forall quantify [x] as it changes for + Optionally, it can also universally quantify over any of our variables + before performing induction. We here forall quantify [x] as it changes for every recursive call. *) iLöb as "IH" forall (x). diff --git a/theories/later.v b/theories/later.v index 152f7fa..d7e033f 100644 --- a/theories/later.v +++ b/theories/later.v @@ -187,8 +187,8 @@ Proof. (** The tactic for Löb induction, [iLöb], requires us to specify the name of the induction hypothesis, which we here call ["IH"]. - Optionally, it can also forall quantify any of our variables before - performing induction. We here forall quantify [x] as it changes for + Optionally, it can also universally quantify over any of our variables + before performing induction. We here forall quantify [x] as it changes for every recursive call. *) iLöb as "IH" forall (x).