diff options
Diffstat (limited to 'tests/lean/misc/loops/Loops/Clauses')
| -rw-r--r-- | tests/lean/misc/loops/Loops/Clauses/Template.lean | 2 |
1 files changed, 1 insertions, 1 deletions
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 |