summaryrefslogtreecommitdiff
path: root/tests/lean
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean')
-rw-r--r--tests/lean/Issue194RecursiveStructProjector.lean35
-rw-r--r--tests/lean/Matches.lean16
2 files changed, 51 insertions, 0 deletions
diff --git a/tests/lean/Issue194RecursiveStructProjector.lean b/tests/lean/Issue194RecursiveStructProjector.lean
new file mode 100644
index 00000000..4eb23934
--- /dev/null
+++ b/tests/lean/Issue194RecursiveStructProjector.lean
@@ -0,0 +1,35 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [issue_194_recursive_struct_projector]
+import Base
+open Primitives
+
+namespace issue_194_recursive_struct_projector
+
+/- [issue_194_recursive_struct_projector::AVLNode]
+ Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 2:0-2:17 -/
+inductive AVLNode (T : Type) :=
+| mk : T → Option (AVLNode T) → Option (AVLNode T) → AVLNode T
+
+@[simp, reducible]
+def AVLNode.value {T : Type} (x : AVLNode T) :=
+ match x with | AVLNode.mk x1 _ _ => x1
+
+@[simp, reducible]
+def AVLNode.left {T : Type} (x : AVLNode T) :=
+ match x with | AVLNode.mk _ x1 _ => x1
+
+@[simp, reducible]
+def AVLNode.right {T : Type} (x : AVLNode T) :=
+ match x with | AVLNode.mk _ _ x1 => x1
+
+/- [issue_194_recursive_struct_projector::get_val]:
+ Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 10:0-10:33 -/
+def get_val (T : Type) (x : AVLNode T) : Result T :=
+ Result.ok x.value
+
+/- [issue_194_recursive_struct_projector::get_left]:
+ Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 14:0-14:43 -/
+def get_left (T : Type) (x : AVLNode T) : Result (Option (AVLNode T)) :=
+ Result.ok x.left
+
+end issue_194_recursive_struct_projector
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