diff options
| author | Son Ho | 2023-03-07 08:41:57 +0100 |
|---|---|---|
| committer | Son HO | 2023-06-04 21:44:33 +0200 |
| commit | feb60683216a6d9193d6353605560c6c80a1ab41 (patch) | |
| tree | 222f61e4c5cbcd166e81d82350afc54b002774df /tests/lean/misc/loops/Loops/Clauses | |
| parent | b4bad8df4eabb17c71dfa7b24d79d62fc06d0a70 (diff) | |
Make minor modifications and regenerate the Lean files
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 |