Drop unnecessary try

opencompl · Mar 26, 2024 · b46797e · b46797e
1 parent 791d8a1
commit b46797e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/SSA/Projects/Scf/ScfFunctor.lean b/SSA/Projects/Scf/ScfFunctor.lean
@@ -537,7 +537,7 @@ open ScfRegion in
 theorem correct :
     Com.denote (lhs rgn niters1 niters2 start1) Γv = Com.denote (rhs rgn niters1 niters2 start1) Γv := by
   simp [lhs, rhs, for_, axpy, cst]
-  try simp_peephole [add, iterate, for_, axpy, cst, cst_nat] at Γv
+  simp_peephole [add, iterate, for_, axpy, cst, cst_nat] at Γv
   intros a
   have swap_niters := add_comm (a := niters1) (b := niters2)
   set arg := ((LoopBody.CounterDecorator 1 fun i v =>