From 35952f29418a9cdcccc49fec9dee223ba0bb3c8c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 4 Mar 2017 15:06:36 -0800 Subject: [PATCH] test(tests/lean/run/ginductive_pred): mutually inductive predicates @dselsam We do not have a "story" for this kind of inductive definition. --- tests/lean/run/ginductive_pred.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 tests/lean/run/ginductive_pred.lean diff --git a/tests/lean/run/ginductive_pred.lean b/tests/lean/run/ginductive_pred.lean new file mode 100644 index 0000000000..2db4af17d8 --- /dev/null +++ b/tests/lean/run/ginductive_pred.lean @@ -0,0 +1,14 @@ +inductive term : Type +| var : nat → term +| app : string → list term → term + +/- In the current system, it will be hard to work with mutually inductive predicates. + Reason: we cannot use well-founded recursion, and the induction principle for it + is too weak. -/ +mutual inductive var_occ, var_occ_list +with var_occ : nat → term → Prop +| leaf (n : nat) : var_occ n (term.var n) +| app (n : nat) (s : string) (ts : list term) : var_occ_list n ts → var_occ n (term.app s ts) +with var_occ_list : nat → list term → Prop +| head (n : nat) (t : term) (ts : list term) : var_occ n t → var_occ_list n (t::ts) +| tail (n : nat) (t : term) (ts : list term) : var_occ_list n ts → var_occ_list n (t::ts)