Skip to content

Commit 5567f58

Browse files
committed
chore: delete stray innacurate comment
1 parent 5311207 commit 5567f58

File tree

1 file changed

+0
-1
lines changed

1 file changed

+0
-1
lines changed

SSA/Projects/Scf/Scf.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -376,7 +376,6 @@ theorem add_iterate (v0 : Int) (b : Int) (a : ℕ) :
376376
simp [ah]
377377
linarith
378378

379-
/-- Reverse a loop. -/
380379
theorem correct :
381380
Com.denote (lhs v0) Γv = Com.denote (rhs v0) Γv := by
382381
simp [lhs, rhs, for_, axpy, cst]

0 commit comments

Comments
 (0)