Update error message in lec4_advanced

tchajed · tchajed · commit 17dd02fd05e1 · 2023-09-27T11:25:21.000-05:00
diff --git a/src/lec4_advanced.dfy b/src/lec4_advanced.dfy
@@ -108,7 +108,7 @@ opaque predicate Good(n: nat) {
 
 lemma FourIsGood_attempt1()
   ensures Good(4)
-{ // error: A postcondition might not hold on this return path
+{ // error: A postcondition could not be proved on this return path
   // notice that this proof doesn't go through - Dafny doesn't know anything
   // about Good other than it is a deterministic predicate that takes a `nat`.
 }

Original file line number	Diff line number	Diff line change
`@@ -108,7 +108,7 @@ opaque predicate Good(n: nat) {`
`108`	`108`
`109`	`109`	`lemma FourIsGood_attempt1()`
`110`	`110`	`ensures Good(4)`
`111`		`-{ // error: A postcondition might not hold on this return path`
	`111`	`+{ // error: A postcondition could not be proved on this return path`
`112`	`112`	`// notice that this proof doesn't go through - Dafny doesn't know anything`
`113`	`113`	// about Good other than it is a deterministic predicate that takes a `nat`.
`114`	`114`	`}`