From a46d785eb548043535a05d1b67dde48c18f5cf5f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 18:46:08 +0200
Subject: Add an example

---
 backends/lean/Base/Primitives/ScalarNotations.lean | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'backends')

diff --git a/backends/lean/Base/Primitives/ScalarNotations.lean b/backends/lean/Base/Primitives/ScalarNotations.lean
index 50d8c1b6..cc6e6f02 100644
--- a/backends/lean/Base/Primitives/ScalarNotations.lean
+++ b/backends/lean/Base/Primitives/ScalarNotations.lean
@@ -84,4 +84,7 @@ example {ty} (x : Scalar ty) : Bool :=
 -- Testing the notations
 example : Result Usize := 0#usize + 1#usize
 
+-- More complex expressions
+example (x y : Int) (h : 0 ≤ x + y ∧ x + y ≤ 1000) : U32 := (x + y)#u32
+
 end Primitives
-- 
cgit v1.2.3