From 942cb272f56ad3d332dee1e55383ec0af25e50b7 Mon Sep 17 00:00:00 2001 From: Anthony Wang Date: Mon, 12 Jan 2026 17:10:34 -0600 Subject: [PATCH] fix: typo in VCGen/Tutorial.lean --- Manual/VCGen/Tutorial.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/VCGen/Tutorial.lean b/Manual/VCGen/Tutorial.lean index 17591abee..f5d6fb89e 100644 --- a/Manual/VCGen/Tutorial.lean +++ b/Manual/VCGen/Tutorial.lean @@ -662,7 +662,7 @@ So there are two reasonable options, inspired by non-termination in traditional : The {tech}_partial correctness interpretation_ - {lean}`⦃P⦄ prog ⦃⇓ r => Q' r⦄` asserts that, given {lean}`P` holds, and _if_ {lean}`prog` terminates _then_ {lean}`Q'` holds for the result. + {lean}`⦃P⦄ prog ⦃⇓? r => Q' r⦄` asserts that, given {lean}`P` holds, and _if_ {lean}`prog` terminates _then_ {lean}`Q'` holds for the result. The notation {lean}`⇓ r => Q' r` has the total interpretation, while {lean}`⇓? r => Q' r` has the partial interpretation.