Merge branch 'main' into son/loops2

1 files changed, 16 insertions, 0 deletions

diff --git a/tests/lean/Matches.lean b/tests/lean/Matches.lean
new file mode 100644
index 00000000..3e3a558b
--- /dev/null
+++ b/tests/lean/Matches.lean
@@ -0,0 +1,16 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [matches]
+import Base
+open Primitives
+
+namespace matches
+
+/- [matches::match_u32]:
+   Source: 'tests/src/matches.rs', lines 4:0-4:27 -/
+def match_u32 (x : U32) : Result U32 :=
+  match x with
+  | 0#u32 => Result.ok 0#u32
+  | 1#u32 => Result.ok 1#u32
+  | _ => Result.ok 2#u32
+
+end matches