tests/src/issue-194-recursive-struct-projector.rs


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

//@ [coq,fstar] subdir=misc
struct AVLNode<T> {
    value: T,
    left: AVLTree<T>,
    right: AVLTree<T>,
}

type AVLTree<T> = Option<Box<AVLNode<T>>>;

fn get_val<T>(x: AVLNode<T>) -> T {
    x.value
}

fn get_left<T>(x: AVLNode<T>) -> AVLTree<T> {
    x.left
}