From 49b14e9f42e626c03fa863354e07e28a756b1413 Mon Sep 17 00:00:00 2001
From: Simon Spies <simonspies@icloud.com>
Date: Mon, 4 Nov 2024 13:55:16 +0100
Subject: [PATCH] tweak

---
 theories/examples/termination/eventloop.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/examples/termination/eventloop.v b/theories/examples/termination/eventloop.v
index be19d594..5e19a2ed 100644
--- a/theories/examples/termination/eventloop.v
+++ b/theories/examples/termination/eventloop.v
@@ -166,7 +166,7 @@ Section open_example.
   Definition example : expr :=
     let: "n" := external_code #() in
     for: "n" do
-      enqueue q (λ: <>, print "Hello World!").
+      enqueue q (λ: <>, print #42).
 
   Lemma for_zero e:
     sbi_emp_valid (WP (for: #0 do e)%V [{ v, ⌜v = #()⌝ }])%I.
@@ -189,7 +189,7 @@ Section open_example.
   Qed.
 
   Lemma example_spec `{FiniteBoundedExistential SI}:
-    queue N q ∗ $ (omul (one: ordA SI)) ∗ SEQ external_code #() [{ v, ∃ n: nat, ⌜v = #n⌝ }] ∗ (□ ∀ s: string, SEQ print s [{ _, True }]) ⊢
+    queue N q ∗ $ (omul (one: ordA SI)) ∗ SEQ external_code #() [{ v, ∃ n: nat, ⌜v = #n⌝ }] ∗ (□ ∀ n: Z, SEQ print #n [{ _, True }]) ⊢
     SEQ example [{ _, True }].
   Proof.
     iIntros "(#Q & Hc & Hwp & #Hprint) Hna". rewrite /example.
-- 
GitLab