From f7c09787c4a7457568d3d79d38b45caac4af8772 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 4 Aug 2023 18:19:37 +0200
Subject: Start adding support for Arrays/Slices in the Lean library

---
 backends/lean/Base/Arith/Scalar.lean | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'backends/lean/Base/Arith/Scalar.lean')

diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean
index b792ff21..db672489 100644
--- a/backends/lean/Base/Arith/Scalar.lean
+++ b/backends/lean/Base/Arith/Scalar.lean
@@ -46,4 +46,8 @@ example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
 example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
   scalar_tac
 
+-- Checking that we explore the goal *and* projectors correctly
+example (x : U32 × U32) : 0 ≤ x.fst.val := by
+  scalar_tac
+
 end Arith
-- 
cgit v1.2.3