add assume to switch

jsiek · Jan 9, 2025 · 947da7e · 947da7e
1 parent f82dc3d
commit 947da7e
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/doc/Reference.md b/doc/Reference.md
@@ -1726,10 +1726,10 @@ theorem switch_proof_example: all x:Nat. x = 0 or 0 < x
 proof
   arbitrary x:Nat
   switch x {
-    case zero {
+    case 0 assume xz: x = 0 {
       conclude true or 0 < 0 by .
     }
-    case suc(x') {
+    case suc(x') assume xs: x = suc(x') {
       have z_l_sx: 0 < suc(x')
           by definition {operator <, operator ≤, operator ≤}
       conclude suc(x') = 0 or 0 < suc(x') by z_l_sx