From 7307b02fd7e518eceb80ed96498123c40d729157 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Mar 2022 15:19:01 -0700 Subject: [PATCH] fix: missing test at `has_trivial_structure` see #1074 --- src/library/compiler/util.cpp | 2 +- tests/lean/1074b.lean | 12 ++++++++++++ tests/lean/1074b.lean.expected.out | 13 +++++++++++++ 3 files changed, 26 insertions(+), 1 deletion(-) create mode 100644 tests/lean/1074b.lean create mode 100644 tests/lean/1074b.lean.expected.out diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp index ca208c95bd..c4e8d9d44e 100644 --- a/src/library/compiler/util.cpp +++ b/src/library/compiler/util.cpp @@ -448,7 +448,7 @@ optional has_trivial_structure(environment const & env, name const & I inductive_val I_val = env.get(I_name).to_inductive_val(); if (I_val.is_unsafe()) return optional(); - if (I_val.get_ncnstrs() != 1) + if (I_val.get_ncnstrs() != 1 || I_val.is_rec()) return optional(); buffer rel_fields; get_constructor_relevant_fields(env, head(I_val.get_cnstrs()), rel_fields); diff --git a/tests/lean/1074b.lean b/tests/lean/1074b.lean new file mode 100644 index 0000000000..4a3a15899d --- /dev/null +++ b/tests/lean/1074b.lean @@ -0,0 +1,12 @@ +inductive Term +| id: Term -> Term + +inductive Brx: Term -> Prop +| id: Brx z -> Brx (Term.id n) + +def Brx.interp {a} (H: Brx a): Nat := + match a with + | Term.id n => by + have ⟨Hn, Hz⟩: True ∧ Brx z + := by cases H <;> exact ⟨by simp, by assumption⟩; + exact Hz.interp diff --git a/tests/lean/1074b.lean.expected.out b/tests/lean/1074b.lean.expected.out new file mode 100644 index 0000000000..7b964c5375 --- /dev/null +++ b/tests/lean/1074b.lean.expected.out @@ -0,0 +1,13 @@ +1074b.lean:10:30-10:31: error: unknown identifier 'z' +1074b.lean:11:43-11:53: error: tactic 'assumption' failed +a : Term +H : Brx a +n : Term +⊢ Brx (sorryAx Term) +1074b.lean:11:9-11:55: error: unsolved goals +case id +a : Term +H : Brx a +n z✝ : Term +a✝ : Brx z✝ +⊢ True ∧ Brx (sorryAx Term)