diff options
Diffstat (limited to '')
-rw-r--r-- | tests/lean/Issue194RecursiveStructProjector.lean | 35 | ||||
-rw-r--r-- | tests/lean/Matches.lean | 16 |
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 |