tweak

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.