From feb60683216a6d9193d6353605560c6c80a1ab41 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 7 Mar 2023 08:41:57 +0100
Subject: Make minor modifications and regenerate the Lean files

---
 tests/lean/misc/loops/Loops/Clauses/Template.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tests/lean/misc/loops/Loops/Clauses')

diff --git a/tests/lean/misc/loops/Loops/Clauses/Template.lean b/tests/lean/misc/loops/Loops/Clauses/Template.lean
index 3c0f2f7c..d74f71e1 100644
--- a/tests/lean/misc/loops/Loops/Clauses/Template.lean
+++ b/tests/lean/misc/loops/Loops/Clauses/Template.lean
@@ -35,7 +35,7 @@ macro_rules
 | `(tactic| sum_with_shared_borrows_loop_decreases $max $i $s) =>`(tactic| sorry)
 
 /- [loops::clear]: termination measure -/
-@[simp] def clear_loop_terminates (v : vec UInt32) (i : USize) := (v, i)
+@[simp] def clear_loop_terminates (v : Vec UInt32) (i : USize) := (v, i)
 
 syntax "clear_loop_decreases" term+ : tactic
 
-- 
cgit v1.2.3