diff options
Diffstat (limited to 'backends/lean/Base')
| -rw-r--r-- | backends/lean/Base/Primitives/ScalarNotations.lean | 3 |
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 |