From aa63fda835eb974bffd7c2c192730866ffdd8c45 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 14 Feb 2022 12:02:39 -0800 Subject: [PATCH] fix: mark auxiliary `noConfusion` declarations for enumeration types as `[reducible]` closes #1016 --- src/Lean/Meta/Constructions.lean | 3 +++ tests/lean/run/1016.lean | 5 +++++ 2 files changed, 8 insertions(+) create mode 100644 tests/lean/run/1016.lean diff --git a/src/Lean/Meta/Constructions.lean b/src/Lean/Meta/Constructions.lean index ec665b3d95..85ef5e885c 100644 --- a/src/Lean/Meta/Constructions.lean +++ b/src/Lean/Meta/Constructions.lean @@ -64,6 +64,7 @@ where safety := DefinitionSafety.safe hints := ReducibilityHints.abbrev } + setReducibleAttribute declName mkNoConfusionType : MetaM Unit := do let enumType := mkConst enumName @@ -83,6 +84,7 @@ where safety := DefinitionSafety.safe hints := ReducibilityHints.abbrev } + setReducibleAttribute declName mkNoConfusion : MetaM Unit := do let enumType := mkConst enumName @@ -105,6 +107,7 @@ where safety := DefinitionSafety.safe hints := ReducibilityHints.abbrev } + setReducibleAttribute declName def mkNoConfusion (declName : Name) : MetaM Unit := do if (← isEnumType declName) then diff --git a/tests/lean/run/1016.lean b/tests/lean/run/1016.lean new file mode 100644 index 0000000000..cb57cda9f9 --- /dev/null +++ b/tests/lean/run/1016.lean @@ -0,0 +1,5 @@ +inductive t | one | two + +example (h : False) : t.one = t.two := by + simp + contradiction