blob: d1a074491c1c463ed336e20c3bd7ce138019f426 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
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.
|
