From bae875980066dfb838693f3eb13f858beec021f0 Mon Sep 17 00:00:00 2001 From: tydeu Date: Sun, 10 Mar 2024 16:52:42 -0400 Subject: [PATCH] feat: allow `noncomputable unsafe` definitions --- src/Lean/Elab/MutualDef.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index edb8e7e94fc8..d58193aa5eb7 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -68,8 +68,6 @@ private def check (prevHeaders : Array DefViewElabHeader) (newHeader : DefViewEl throwError "'partial' theorems are not allowed, 'partial' is a code generation directive" if newHeader.kind.isTheorem && newHeader.modifiers.isNoncomputable then throwError "'theorem' subsumes 'noncomputable', code is not generated for theorems" - if newHeader.modifiers.isNoncomputable && newHeader.modifiers.isUnsafe then - throwError "'noncomputable unsafe' is not allowed" if newHeader.modifiers.isNoncomputable && newHeader.modifiers.isPartial then throwError "'noncomputable partial' is not allowed" if newHeader.modifiers.isPartial && newHeader.modifiers.isUnsafe then