Equations
-
Lean.Elab.Tactic.Conv.evalPattern stx = Lean.Elab.Tactic.withMainContext
(let discr := stx;
if Lean.Syntax.isOfKind discr `Lean.Parser.Tactic.Conv.pattern = true then
let discr_1 := Lean.Syntax.getArg discr 0;
let discr := Lean.Syntax.getArg discr 1;
let p := discr;
do
let patternA ←
withTheReader Lean.Elab.Term.Context
(fun ctx =>
{ fileName := ctx.fileName, fileMap := ctx.fileMap, declName? := ctx.declName?,
macroStack := ctx.macroStack, currMacroScope := ctx.currMacroScope, mayPostpone := ctx.mayPostpone,
errToSorry := ctx.errToSorry, autoBoundImplicit := ctx.autoBoundImplicit,
autoBoundImplicits := ctx.autoBoundImplicits, sectionVars := ctx.sectionVars,
sectionFVars := ctx.sectionFVars, implicitLambda := ctx.implicitLambda,
isNoncomputableSection := ctx.isNoncomputableSection, ignoreTCFailures := true })
(liftM
(Lean.Elab.Term.withoutModifyingElabMetaStateWithInfo
(Lean.withRef p
(Lean.Elab.Term.withoutErrToSorry do
let a ← Lean.Elab.Term.elabTerm p none true true
liftM (Lean.Meta.abstractMVars a)))))
let lhs ← Lean.Elab.Tactic.Conv.getLhs
let a ← liftM (Lean.Elab.Tactic.Conv.findPattern? patternA lhs)
match a with
| none =>
Lean.throwError
(Lean.toMessageData "'pattern' conv tactic failed, pattern was not found" ++ Lean.toMessageData (Lean.indentExpr patternA.expr) ++ Lean.toMessageData "")
| some (mvarId', result) => do
let a ← liftM (Lean.Meta.Simp.Result.getProof result)
Lean.Elab.Tactic.Conv.updateLhs result.expr a
let a ← Lean.Elab.Tactic.getMainGoal
liftM (Lean.Meta.applyRefl a (Function.comp Lean.MessageData.ofFormat Lean.format "refl failed"))
Lean.Elab.Tactic.replaceMainGoal [mvarId']
else
let discr := stx;
Lean.Elab.throwUnsupportedSyntax)