max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: do not have meta imply partial (#11587)

Browse source 
This PR adjusts the new `meta` keyword of the experimental module system
not to imply `partial` for general consistency.

As the previous behavior can create confusion return types that are not
known to be `Nonempty` and few `def`s should be `meta` in the first
case, this special case does not appear to be worth the minor
convenience.
This commit is contained in:
Sebastian Ullrich 2025-12-12 12:42:42 +01:00 • committed by GitHub
parent 9f74e71f10
commit 520cdb2038
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 6 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Lean/Elab/DeclModifiers.lean
View file

@ -103,15 +103,6 @@ def Modifiers.isPartial : Modifiers → Bool
| { recKind := .partial, .. } => true
| _ => false
/--
Whether the declaration is explicitly `partial` or should be considered as such via `meta`. In the
latter case, elaborators should not produce an error if partiality is unnecessary.
-/
def Modifiers.isInferredPartial : Modifiers → Bool
| { recKind := .partial, .. } => true
| { computeKind := .meta, .. } => true
| _ => false
def Modifiers.isNonrec : Modifiers → Bool
| { recKind := .nonrec, .. } => true
| _ => false

24
src/Lean/Elab/PreDefinition/Main.lean
View file

@ -329,25 +329,13 @@ def addPreDefinitions (docCtx : LocalContext × LocalInstances) (preDefs : Array
else if preDefs.any (·.modifiers.isUnsafe) then
addAndCompileUnsafe docCtx preDefs
preDefs.forM (·.termination.ensureNone "unsafe")
else if preDefs.any (·.modifiers.isPartial) then
for preDef in preDefs do
if preDef.modifiers.isPartial && !(← whnfD preDef.type).isForall then
withRef preDef.ref <| throwError "invalid use of `partial`, `{preDef.declName}` is not a function{indentExpr preDef.type}"
addAndCompilePartial docCtx preDefs
preDefs.forM (·.termination.ensureNone "partial")
else
-- Consider partial if `partial` was given explicitly, or implied and no termination hint
-- was given
if preDefs.any (·.modifiers.isPartial) ||
preDefs.any (·.modifiers.isInferredPartial) && !preDefs.any (·.termination.isNotNone) then
let mut isPartial := true
for preDef in preDefs do
if !(← whnfD preDef.type).isForall then
if preDef.modifiers.isPartial then
withRef preDef.ref <| throwError "invalid use of `partial`, `{preDef.declName}` is not a function{indentExpr preDef.type}"
else
-- `meta` should not imply `partial` in this case
isPartial := false
if isPartial then
addAndCompilePartial docCtx preDefs
preDefs.forM (·.termination.ensureNone "partial")
continue
ensureFunIndReservedNamesAvailable preDefs
try
checkCodomainsLevel preDefs