From 55266277a6d6a7b29cc40338fa4c68e78a0943e6 Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Thu, 22 Feb 2024 14:55:11 -0600
Subject: [PATCH] Fix bug in smt-lib example
---
spec/doc.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/spec/doc.tex b/spec/doc.tex
index a50de4a..f68c66c 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -663,7 +663,7 @@ An Alethe proof is a list of commands.
(assume h1 (not (p a)))
(assume h2 (forall ((z1 U)) (forall ((z2 U)) (p z2))))
...
-(anchor :step t9 :args ((:= z2 vr4)))
+(anchor :step t9 :args ((vr4 U) (:= z2 vr4)))
(step t9.t1 (cl (= z2 vr4)) :rule refl)
(step t9.t2 (cl (= (p z2) (p vr4)))
:rule cong :premises (t9.t1))
--
GitLab