From fb1cb3c623f4fa8798251b7beefa46e93e2fa966 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 6 Jan 2015 11:55:31 -0800 Subject: [PATCH] test(tests/lean/run): define tree_list length function using recursive equations tree_list is part of a mutually inductive datatype. --- tests/lean/run/eq23.lean | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 tests/lean/run/eq23.lean diff --git a/tests/lean/run/eq23.lean b/tests/lean/run/eq23.lean new file mode 100644 index 0000000000..e1a44aafce --- /dev/null +++ b/tests/lean/run/eq23.lean @@ -0,0 +1,29 @@ +open nat + +inductive tree (A : Type) := +leaf : A → tree A, +node : tree_list A → tree A +with tree_list := +nil : tree_list A, +cons : tree A → tree_list A → tree_list A + +namespace tree_list + +definition len {A : Type} : tree_list A → nat, +len (nil A) := 0, +len (cons t l) := len l + 1 + +theorem len_nil {A : Type} : len (nil A) = 0 := +rfl + +theorem len_cons {A : Type} (t : tree A) (l : tree_list A) : len (cons t l) = len l + 1 := +rfl + +variables (A : Type) (t1 t2 t3 : tree A) + +example : len (cons t1 (cons t2 (cons t3 (nil A)))) = 3 := +rfl + +print definition len + +end tree_list