We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 63975f7 commit 0cb1c10Copy full SHA for 0cb1c10
CaseStudies/Velvet/VelvetExamples/Demo/IsNonPrime.lean
@@ -69,7 +69,7 @@ method IsNonPrime (n: Nat)
69
-- Program verification
70
------------------------------------------------
71
72
-theorem goal
+theorem remaining_goal
73
(n : ℕ)
74
(i : ℕ)
75
(ret : Bool)
@@ -138,4 +138,4 @@ theorem goal
138
139
prove_correct IsNonPrime by
140
loom_solve; try simp_all
141
- apply (goal n i ret i_1 ret_1 if_neg invariant_1 invariant_2 invariant_3 done_1 i_2)
+ apply (remaining_goal n i ret i_1 ret_1 if_neg invariant_1 invariant_2 invariant_3 done_1 i_2)
0 commit comments