diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index dfd836c73c..4c49d4c792 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -743,7 +743,7 @@ structure State where abbrev M := ReaderT Context $ StateRefT State TermElabM /-- Infer the `motive` using the expected type by `kabstract`ing the discriminants. -/ -def mkMotive (discrs : Array Expr) (expectedType : Expr): MetaM Expr := do +def mkMotive (discrs : Array Expr) (expectedType : Expr) : MetaM Expr := do discrs.foldrM (init := expectedType) fun discr motive => do let discr ← instantiateMVars discr let motiveBody ← kabstract motive discr @@ -878,7 +878,16 @@ partial def main : M Expr := do main let idx := (← get).idx if (← read).elimInfo.motivePos == idx then - let motive ← mkImplicitArg binderType binderInfo + let motive ← + match (← getNextArg? binderName binderInfo) with + | .some arg => + /- Due to `Lean.Elab.Term.elabAppArgs.elabAsElim?`, this must be a positional argument that is the syntax `_`. -/ + elabArg arg binderType + | .none | .undef => + /- Note: undef occurs when the motive is explicit but missing. + In this case, we treat it as if it were an implicit argument + to support writing `h.rec` when `h : False`, rather than requiring `h.rec _`. -/ + mkImplicitArg binderType binderInfo setMotive motive addArgAndContinue motive else if let some tidx := (← read).elimInfo.targetsPos.indexOf? idx then @@ -970,15 +979,34 @@ where unless (← shouldElabAsElim declName) do return none let elimInfo ← getElimInfo declName forallTelescopeReducing (← inferType f) fun xs _ => do - if h : elimInfo.motivePos < xs.size then - let x := xs[elimInfo.motivePos] + /- Process arguments similar to `Lean.Elab.Term.ElabElim.main` to see if the motive has been + provided, in which case we use the standard app elaborator. + If the motive is explicit (like for `False.rec`), then a positional `_` counts as "not provided". -/ + let mut args := args.toList + let mut namedArgs := namedArgs.toList + for x in xs[0:elimInfo.motivePos] do let localDecl ← x.fvarId!.getDecl - if findBinderName? namedArgs.toList localDecl.userName matches some _ then + match findBinderName? namedArgs localDecl.userName with + | some _ => namedArgs := eraseNamedArg namedArgs localDecl.userName + | none => if localDecl.binderInfo.isExplicit then args := args.tailD [] + -- Invariant: `elimInfo.motivePos < xs.size` due to construction of `elimInfo`. + let some x := xs[elimInfo.motivePos]? | unreachable! + let localDecl ← x.fvarId!.getDecl + if findBinderName? namedArgs localDecl.userName matches some _ then + -- motive has been explicitly provided, so we should use standard app elaborator + return none + else + match localDecl.binderInfo.isExplicit, args with + | true, .expr _ :: _ => -- motive has been explicitly provided, so we should use standard app elaborator return none - return some elimInfo - else - return none + | true, .stx arg :: _ => + if arg.isOfKind ``Lean.Parser.Term.hole then + return some elimInfo + else + -- positional motive is not `_`, so we should use standard app elaborator + return none + | _, _ => return some elimInfo /-- Collect extra argument positions that must be elaborated eagerly when using `elab_as_elim`. diff --git a/tests/lean/276.lean b/tests/lean/276.lean index bae43741a8..aeae650d0e 100644 --- a/tests/lean/276.lean +++ b/tests/lean/276.lean @@ -5,5 +5,5 @@ set_option pp.all true in #check fun {α : Sort v} => PEmpty.rec (fun _ => α) -- but `def` doesn't work --- error: (kernel) compiler failed to infer low level type, unknown declaration 'PEmpty.rec' +-- error: code generator does not support recursor 'PEmpty.rec' yet def PEmpty.elim' {α : Sort v} := PEmpty.rec (fun _ => α) diff --git a/tests/lean/276.lean.expected.out b/tests/lean/276.lean.expected.out index 35e51a5f70..cea833efcd 100644 --- a/tests/lean/276.lean.expected.out +++ b/tests/lean/276.lean.expected.out @@ -1,3 +1,2 @@ -276.lean:5:27-5:50: error: failed to elaborate eliminator, expected type is not available -fun {α : Sort v} => @?m α : {α : Sort v} → @?m α -276.lean:9:33-9:56: error: failed to elaborate eliminator, expected type is not available +fun {α : Sort v} => PEmpty.rec.{v, u_1} fun (x : PEmpty.{u_1}) => α : {α : Sort v} → PEmpty.{u_1} → α +276.lean:9:4-9:16: error: code generator does not support recursor 'PEmpty.rec' yet, consider using 'match ... with' and/or structural recursion diff --git a/tests/lean/run/1697.lean b/tests/lean/run/1697.lean index 23534e4551..bb8d15715c 100644 --- a/tests/lean/run/1697.lean +++ b/tests/lean/run/1697.lean @@ -8,7 +8,7 @@ error: cannot evaluate expression that depends on the `sorry` axiom. Use `#eval!` to evaluate nevertheless (which may cause lean to crash). -/ #guard_msgs in -#eval show Nat from False.rec (by decide) +#eval show Nat from False.elim (by decide) /-- warning: declaration uses 'sorry' diff --git a/tests/lean/run/elabAsElim.lean b/tests/lean/run/elabAsElim.lean index b76607fcf5..d3585e3750 100644 --- a/tests/lean/run/elabAsElim.lean +++ b/tests/lean/run/elabAsElim.lean @@ -175,3 +175,14 @@ def leRecOn {C : Nat → Sort _} {n : Nat} : ∀ {m}, n ≤ m → (∀ {k}, C k theorem leRecOn_self {C : Nat → Sort _} {n} {next : ∀ {k}, C k → C (k + 1)} (x : C n) : (leRecOn n.le_refl next x : C n) = x := sorry + +/-! +Issue https://github.com/leanprover/lean4/issues/4347 + +`False.rec` has `motive` as an explicit argument. +-/ + +example (h : False) : Nat := False.rec (fun _ => Nat) h +example (h : False) : Nat := False.rec _ h +example (h : False) : Nat := h.rec +example (h : False) : Nat := h.rec _ diff --git a/tests/lean/run/emptyLcnf.lean b/tests/lean/run/emptyLcnf.lean index e3fd9967eb..01d5f5ebd8 100644 --- a/tests/lean/run/emptyLcnf.lean +++ b/tests/lean/run/emptyLcnf.lean @@ -3,7 +3,7 @@ import Lean inductive MyEmpty def f (x : MyEmpty) : Nat := - MyEmpty.casesOn x + MyEmpty.casesOn _ x set_option trace.Compiler.result true /--