Lean4
@[command_elab Mathlib.Tactic.Recall.recall]
public meta def _aux_Mathlib_Tactic_Recall___elabRules_Mathlib_Tactic_Recall_recall_1 :
Lean.Elab.Command.CommandElab✝ := fun
| `(recall $id$sig:optDeclSig$[$val?]?) =>
withoutModifyingEnv
(do
let declName := id.getId
let some info := (← getEnv).find? declName |
throwError "unknown constant '{declName}'"
let declConst : Expr := mkConst declName <| info.levelParams.map Level.param
discard <| liftTermElabM <| addTermInfo id declConst
let newId := ({ namePrefix := declName : DeclNameGenerator }.mkUniqueName (← getEnv) `recall).1
let newId := mkIdentFrom id newId
if let some val := val? then
let some infoVal := info.value? |
throwErrorAt val "constant '{declName}' has no defined value"
elabCommand <| ← `(noncomputable def $newId$sig:optDeclSig$val)
let some newInfo := (← getEnv).find? newId.getId |
return -- def already threw
liftTermElabM do
let mvs ← newInfo.levelParams.mapM fun _ => mkFreshLevelMVar
let newType := newInfo.type.instantiateLevelParams newInfo.levelParams mvs
unless (← isDefEq info.type newType) do
throwTypeMismatchError none info.type newInfo.type declConst
let newVal := newInfo.value?.get!.instantiateLevelParams newInfo.levelParams mvs
unless (← isDefEq infoVal newVal) do
let err :=
m!"\
value mismatch{(indentExpr declConst)}\nhas value{(indentExpr newVal)}\n\
but is expected to have value{indentExpr infoVal}"
throwErrorAt val
else
let (binders, type?) := expandOptDeclSig sig
if let some type := type? then
runTermElabM fun vars => do
withAutoBoundImplicit do
elabBinders binders.getArgs fun xs => do
let xs ← addAutoBoundImplicits xs none
let type ← elabType type
Term.synthesizeSyntheticMVarsNoPostponing
let type ← mkForallFVars xs type
let type ← mkForallFVars vars type (usedOnly := true)
unless (← isDefEq info.type type) do
throwTypeMismatchError none info.type type declConst
else
unless binders.getNumArgs == 0 do
throwError "expected type after ':'")
| _ => no_error_if_unused% throwUnsupportedSyntax✝
