Documentation

Lean.Elab.Tactic.Match

def Lean.Elab.Tactic.evalEraseAuxDiscrs :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalEraseAuxDiscrs x = Lean.Elab.Tactic.withMainContext do let lctx ← Lean.getLCtx let auxDecls : List Lean.FVarId := Lean.LocalContext.foldl lctx (fun auxDecls localDecl => if Lean.Elab.Term.isAuxDiscrName (Lean.LocalDecl.userName localDecl) = true then Lean.LocalDecl.fvarId localDecl :: auxDecls else auxDecls) [] let mvarId ← Lean.Elab.Tactic.getMainGoal let r ← forIn auxDecls mvarId fun auxDecl r => let mvarId := r; do let r ← liftM (Lean.Meta.tryClear mvarId auxDecl) let mvarId : Lean.MVarId := r pure PUnit.unit pure (ForInStep.yield mvarId) let x : Lean.MVarId := r let mvarId : Lean.MVarId := x Lean.Elab.Tactic.replaceMainGoal [mvarId]

structure Lean.Elab.Tactic.AuxMatchTermState :

Type

nextIdx : Nat
cases : Array Lean.Syntax

def Lean.Elab.Tactic.evalMatch :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalMatch stx = do let tag ← Lean.Elab.Tactic.getMainTag let discr ← Lean.Elab.liftMacroM (Lean.Elab.Tactic.mkAuxiliaryMatchTerm tag stx) let x : Lean.Syntax × Array Lean.Syntax := discr match x with | (matchTerm, cases) => do let refineMatchTerm ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.refine #[Lean.Syntax.atom info "refine", matchTerm]) let stxNew : Lean.Syntax := Lean.mkNullNode (#[refineMatchTerm] ++ cases) Lean.Elab.Tactic.withMacroExpansion stx stxNew (Lean.Elab.Tactic.evalTactic stxNew)