From 2354341c58da168da7161effe1af7bdaf34d315f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 4 Sep 2016 16:46:11 -0700 Subject: [PATCH] test(tests/lean/run): add test for equation compiler --- tests/lean/run/def_ite_value.lean | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 tests/lean/run/def_ite_value.lean diff --git a/tests/lean/run/def_ite_value.lean b/tests/lean/run/def_ite_value.lean new file mode 100644 index 0000000000..2815a36a97 --- /dev/null +++ b/tests/lean/run/def_ite_value.lean @@ -0,0 +1,21 @@ +set_option new_elaborator true + +inductive bv : nat → Type +| nil : bv 0 +| cons : Π n, bool → bv n → bv (n+1) + +open bv + +definition f : ∀ n : nat, bv n → nat → nat +| (n+1) (cons .n b v) 1000000 := f n v 0 +| (n+1) (cons .n b v) x := f n v (x + 1) +| _ _ _ := 1 + +set_option pp.binder_types true + +check @f._main.equations.eqn_1 +check @f._main.equations.eqn_2 +check @f._main.equations.eqn_3 + +example (n : nat) (b : bool) (v : bv n) (x : nat) : x ≠ 1000000 → f (n+1) (cons n b v) x = f n v (x + 1) := +assume H, f._main.equations.eqn_3 n b v x H