Skip to content

Commit 350bbd0

Browse files
committed
doc: Update default documentation
1 parent 7324176 commit 350bbd0

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

doc/goal.ipynb

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -494,7 +494,7 @@
494494
"def f : Nat -> Nat := sorry\n",
495495
"theorem property (n : Nat) : f n = n + 1 := sorry\n",
496496
"\"\"\"\n",
497-
"target, = await server.load_sorry_async(sketch)\n",
497+
"target, = await server.load_sorry_async(sketch, ignore_values=True)\n",
498498
"print(target.goal_state)"
499499
]
500500
},

0 commit comments

Comments
 (0)