more comments on mul

secure-foundations · Feb 12, 2025 · b7c3d1d · b7c3d1d
1 parent 946256c
commit b7c3d1d
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/tasks/human_eval_013.rs b/tasks/human_eval_013.rs
@@ -11,8 +11,10 @@ use vstd::prelude::*;
 verus! {
 
 // This function is part of the specification
+// It helps Verus automatically choose the correct
+// quantifiers in the code below.
 pub open spec fn mul(a: nat, b: nat) -> nat {
-    builtin::mul(a, b)
+    a * b
 }
 
 // This function is also part of the specification