Merge pull request #82 from AeneasVerif/son/switch

Improve tuple projections and matches over integers in Lean

1 files changed, 1 insertions, 1 deletions

diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index c90a85b8..e1a39d40 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -131,7 +131,7 @@ def Slice.new (α : Type u): Slice α := ⟨ [], by apply Scalar.cMax_suffices .
 
 -- TODO: very annoying that the α is an explicit parameter
 def Slice.len (α : Type u) (v : Slice α) : Usize :=
-  Usize.ofIntCore v.val.len (by scalar_tac) (by scalar_tac)
+  Usize.ofIntCore v.val.len (by constructor <;> scalar_tac)
 
 @[simp]
 theorem Slice.len_val {α : Type u} (v : Slice α) : (Slice.len α v).val = v.length :=