diff options
Diffstat (limited to 'tests/coq/misc')
-rw-r--r-- | tests/coq/misc/Issue194RecursiveStructProjector.v | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/tests/coq/misc/Issue194RecursiveStructProjector.v b/tests/coq/misc/Issue194RecursiveStructProjector.v new file mode 100644 index 00000000..d1a07449 --- /dev/null +++ b/tests/coq/misc/Issue194RecursiveStructProjector.v @@ -0,0 +1,54 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [issue_194_recursive_struct_projector] *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Module Issue194RecursiveStructProjector. + +(** [issue_194_recursive_struct_projector::AVLNode] + Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 2:0-2:17 *) +Inductive AVLNode_t (T : Type) := +| mkAVLNode_t : + T -> + option (AVLNode_t T) -> + option (AVLNode_t T) -> + AVLNode_t T +. + +Arguments mkAVLNode_t { _ }. + +Definition aVLNode_value {T : Type} (x : AVLNode_t T) := + match x with | mkAVLNode_t x1 _ _ => x1 end +. + +Notation "x2 .(aVLNode_value)" := (aVLNode_value x2) (at level 9). + +Definition aVLNode_left {T : Type} (x : AVLNode_t T) := + match x with | mkAVLNode_t _ x1 _ => x1 end +. + +Notation "x2 .(aVLNode_left)" := (aVLNode_left x2) (at level 9). + +Definition aVLNode_right {T : Type} (x : AVLNode_t T) := + match x with | mkAVLNode_t _ _ x1 => x1 end +. + +Notation "x2 .(aVLNode_right)" := (aVLNode_right x2) (at level 9). + +(** [issue_194_recursive_struct_projector::get_val]: + Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 10:0-10:33 *) +Definition get_val (T : Type) (x : AVLNode_t T) : result T := + Ok x.(aVLNode_value) +. + +(** [issue_194_recursive_struct_projector::get_left]: + Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 14:0-14:43 *) +Definition get_left + (T : Type) (x : AVLNode_t T) : result (option (AVLNode_t T)) := + Ok x.(aVLNode_left) +. + +End Issue194RecursiveStructProjector. |