From 25aa847aba15a85bfbc5989d1402f32a18e5725a Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Sun, 23 Jul 2017 09:38:44 +0100 Subject: [PATCH] fix(library/constructions/brec_on): make motive explicit in *.below Otherwise you can't figure out the type from the pretty-printed output `nat.below n`. --- src/library/constructions/brec_on.cpp | 2 + tests/lean/whnf.lean.expected.out | 36 +++++----- tests/lean/whnf_cache_bug.lean.expected.out | 19 ++--- tests/lean/whnf_core1.lean.expected.out | 78 +++++++++++---------- 4 files changed, 72 insertions(+), 63 deletions(-) diff --git a/src/library/constructions/brec_on.cpp b/src/library/constructions/brec_on.cpp index 7254b23071..2efc8a19f2 100644 --- a/src/library/constructions/brec_on.cpp +++ b/src/library/constructions/brec_on.cpp @@ -96,6 +96,8 @@ static environment mk_below(environment const & env, name const & n, bool ibelow args.push_back(ref_args[i]); typeformer_names.push_back(mlocal_name(ref_args[i])); } + // make motive explicit + args[0] = update_local(args[0], {}); // we ignore minor premises in below/ibelow for (unsigned i = nparams + ntypeformers + nminors; i < ref_args.size(); i++) args.push_back(ref_args[i]); diff --git a/tests/lean/whnf.lean.expected.out b/tests/lean/whnf.lean.expected.out index 42c057e145..4a465c0d69 100644 --- a/tests/lean/whnf.lean.expected.out +++ b/tests/lean/whnf.lean.expected.out @@ -1,9 +1,9 @@ succ ((⟨nat.rec - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), - (λ (a a_1 : ℕ) (_F : nat.below a_1), - nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ ((_F.fst).fst a)) + ⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1), + nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), a) + (λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (succ a_1)), succ ((_F.fst).fst a)) _F) a_1 a @@ -11,11 +11,11 @@ succ 0 punit.star, punit.star⟩ - (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below a)), - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), - (λ (a a_1 : ℕ) (_F : nat.below a_1), - nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ ((_F.fst).fst a)) + (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below (λ (a : ℕ), ℕ → ℕ) a)), + ⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1), + nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), a) + (λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (succ a_1)), succ ((_F.fst).fst a)) _F) a_1 a @@ -29,10 +29,10 @@ succ 3 succ ((⟨nat.rec - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), - (λ (a a_1 : ℕ) (_F : nat.below a_1), - nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ ((_F.fst).fst a)) + ⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1), + nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), a) + (λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (succ a_1)), succ ((_F.fst).fst a)) _F) a_1 a @@ -40,11 +40,11 @@ succ 0 punit.star, punit.star⟩ - (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below a)), - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), - (λ (a a_1 : ℕ) (_F : nat.below a_1), - nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ ((_F.fst).fst a)) + (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below (λ (a : ℕ), ℕ → ℕ) a)), + ⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1), + nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), a) + (λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (succ a_1)), succ ((_F.fst).fst a)) _F) a_1 a diff --git a/tests/lean/whnf_cache_bug.lean.expected.out b/tests/lean/whnf_cache_bug.lean.expected.out index a2d1ec1a5d..68f6119be0 100644 --- a/tests/lean/whnf_cache_bug.lean.expected.out +++ b/tests/lean/whnf_cache_bug.lean.expected.out @@ -1,10 +1,10 @@ ?m_1 nat.succ ((⟨nat.rec - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), - (λ (a a_1 : ℕ) (_F : nat.below a_1), - nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F.fst).fst a)) + ⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1), + nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), a) + (λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (nat.succ a_1)), nat.succ ((_F.fst).fst a)) _F) a_1 a @@ -12,11 +12,12 @@ nat.succ 0 punit.star, punit.star⟩ - (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below a)), - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), - (λ (a a_1 : ℕ) (_F : nat.below a_1), - nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F.fst).fst a)) + (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below (λ (a : ℕ), ℕ → ℕ) a)), + ⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1), + nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), a) + (λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (nat.succ a_1)), + nat.succ ((_F.fst).fst a)) _F) a_1 a diff --git a/tests/lean/whnf_core1.lean.expected.out b/tests/lean/whnf_core1.lean.expected.out index 8858339d87..ab6328ad83 100644 --- a/tests/lean/whnf_core1.lean.expected.out +++ b/tests/lean/whnf_core1.lean.expected.out @@ -1,9 +1,9 @@ nat.succ ((⟨nat.rec - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), - (λ (a a_1 : ℕ) (_F : nat.below a_1), - nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F.fst).fst a)) + ⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1), + nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), a) + (λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (nat.succ a_1)), nat.succ ((_F.fst).fst a)) _F) a_1 a @@ -11,11 +11,12 @@ nat.succ 0 punit.star, punit.star⟩ - (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below a)), - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), - (λ (a a_1 : ℕ) (_F : nat.below a_1), - nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F.fst).fst a)) + (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below (λ (a : ℕ), ℕ → ℕ) a)), + ⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1), + nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), a) + (λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (nat.succ a_1)), + nat.succ ((_F.fst).fst a)) _F) a_1 a @@ -24,10 +25,11 @@ nat.succ ⟨ih_1, punit.star⟩, ⟨ih_1, punit.star⟩⟩) ((⟨nat.rec - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), - (λ (a a_1 : ℕ) (_F : nat.below a_1), - nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F.fst).fst a)) + ⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1), + nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), a) + (λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (nat.succ a_1)), + nat.succ ((_F.fst).fst a)) _F) a_1 a @@ -35,11 +37,12 @@ nat.succ 0 punit.star, punit.star⟩ - (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below a)), - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), - (λ (a a_1 : ℕ) (_F : nat.below a_1), - nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F.fst).fst a)) + (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below (λ (a : ℕ), ℕ → ℕ) a)), + ⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1), + nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), a) + (λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (nat.succ a_1)), + nat.succ ((_F.fst).fst a)) _F) a_1 a @@ -54,10 +57,10 @@ nat.succ a) nat.succ ((⟨nat.rec - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), - (λ (a a_1 : ℕ) (_F : nat.below a_1), - nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F.fst).fst a)) + ⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1), + nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), a) + (λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (nat.succ a_1)), nat.succ ((_F.fst).fst a)) _F) a_1 a @@ -65,11 +68,12 @@ nat.succ 0 punit.star, punit.star⟩ - (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below a)), - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), - (λ (a a_1 : ℕ) (_F : nat.below a_1), - nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F.fst).fst a)) + (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below (λ (a : ℕ), ℕ → ℕ) a)), + ⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1), + nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), a) + (λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (nat.succ a_1)), + nat.succ ((_F.fst).fst a)) _F) a_1 a @@ -78,10 +82,11 @@ nat.succ ⟨ih_1, punit.star⟩, ⟨ih_1, punit.star⟩⟩) ((⟨nat.rec - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), - (λ (a a_1 : ℕ) (_F : nat.below a_1), - nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F.fst).fst a)) + ⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1), + nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), a) + (λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (nat.succ a_1)), + nat.succ ((_F.fst).fst a)) _F) a_1 a @@ -89,11 +94,12 @@ nat.succ 0 punit.star, punit.star⟩ - (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below a)), - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), - (λ (a a_1 : ℕ) (_F : nat.below a_1), - nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F.fst).fst a)) + (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below (λ (a : ℕ), ℕ → ℕ) a)), + ⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1), + nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), a) + (λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (nat.succ a_1)), + nat.succ ((_F.fst).fst a)) _F) a_1 a