From c81c96f20b1dbf428a9ed42e83b910e798e1a225 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 27 May 2024 17:33:56 +0200 Subject: Add some tests --- tests/src/issue-194-recursive-struct-projector.rs | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 tests/src/issue-194-recursive-struct-projector.rs (limited to 'tests/src/issue-194-recursive-struct-projector.rs') diff --git a/tests/src/issue-194-recursive-struct-projector.rs b/tests/src/issue-194-recursive-struct-projector.rs new file mode 100644 index 00000000..9ebdc2bc --- /dev/null +++ b/tests/src/issue-194-recursive-struct-projector.rs @@ -0,0 +1,16 @@ +//@ [coq,fstar] subdir=misc +struct AVLNode { + value: T, + left: AVLTree, + right: AVLTree, +} + +type AVLTree = Option>>; + +fn get_val(x: AVLNode) -> T { + x.value +} + +fn get_left(x: AVLNode) -> AVLTree { + x.left +} -- cgit v1.2.3