summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2024-06-12 18:46:08 +0200
committerSon Ho2024-06-12 18:46:08 +0200
commita46d785eb548043535a05d1b67dde48c18f5cf5f (patch)
tree1bb1cad0570ac98decf0f55b7de580fe11c55840
parent19abb19134efe0b16409f955b13af36262f231a8 (diff)
Add an example
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Primitives/ScalarNotations.lean3
1 files changed, 3 insertions, 0 deletions
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