def
Lean.Elab.Tactic.rewriteTarget
(stx : Lean.Syntax)
(symm : Bool)
(config : Lean.Meta.Rewrite.Config)
:
Equations
- Lean.Elab.Tactic.rewriteTarget stx symm config = Lean.Elab.Term.withSynthesize (Lean.Elab.Tactic.withMainContext do let e ← Lean.Elab.Tactic.elabTerm stx none true let a ← Lean.Elab.Tactic.getMainGoal let a_1 ← Lean.Elab.Tactic.getMainTarget let r ← liftM (Lean.Meta.rewrite a a_1 e symm Lean.Occurrences.all config) let a ← Lean.Elab.Tactic.getMainGoal let mvarId' ← liftM (Lean.Meta.replaceTargetEq a r.eNew r.eqProof) Lean.Elab.Tactic.replaceMainGoal (mvarId' :: r.mvarIds))
def
Lean.Elab.Tactic.rewriteLocalDecl
(stx : Lean.Syntax)
(symm : Bool)
(fvarId : Lean.FVarId)
(config : Lean.Meta.Rewrite.Config)
:
Equations
- Lean.Elab.Tactic.rewriteLocalDecl stx symm fvarId config = Lean.Elab.Term.withSynthesize (Lean.Elab.Tactic.withMainContext do let e ← Lean.Elab.Tactic.elabTerm stx none true let localDecl ← liftM (Lean.Meta.getLocalDecl fvarId) let a ← Lean.Elab.Tactic.getMainGoal let rwResult ← liftM (Lean.Meta.rewrite a (Lean.LocalDecl.type localDecl) e symm Lean.Occurrences.all config) let a ← Lean.Elab.Tactic.getMainGoal let replaceResult ← liftM (Lean.Meta.replaceLocalDecl a fvarId rwResult.eNew rwResult.eqProof) Lean.Elab.Tactic.replaceMainGoal (replaceResult.mvarId :: rwResult.mvarIds))
def
Lean.Elab.Tactic.withRWRulesSeq
(token : Lean.Syntax)
(rwRulesSeqStx : Lean.Syntax)
(x : Bool → Lean.Syntax → Lean.Elab.Tactic.TacticM Unit)
:
Equations
- Lean.Elab.Tactic.withRWRulesSeq token rwRulesSeqStx x = let lbrak := Lean.Syntax.getOp rwRulesSeqStx 0; let rules := Lean.Syntax.getArgs (Lean.Syntax.getOp rwRulesSeqStx 1); let rbrak := Lean.Syntax.getOp rwRulesSeqStx 2; do Lean.Elab.Tactic.withTacticInfoContext (Lean.mkNullNode #[token, lbrak]) (pure ()) let numRules : Nat := (Array.size rules + 1) / 2 let r ← let col := { start := 0, stop := numRules, step := 1 }; forIn col PUnit.unit fun i r => let rule := Array.getOp rules (i * 2); let sep := Array.getD rules (i * 2 + 1) Lean.Syntax.missing; do Lean.Elab.Tactic.withTacticInfoContext (Lean.mkNullNode #[rule, sep]) (Lean.withRef rule (let symm := !Lean.Syntax.isNone (Lean.Syntax.getOp rule 0); let term := Lean.Syntax.getOp rule 1; x symm term)) pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit
Equations
- Lean.Elab.Tactic.elabRewriteConfig optConfig = if Lean.Syntax.isNone optConfig = true then pure { transparency := Lean.Meta.TransparencyMode.reducible, offsetCnstrs := true } else Lean.withoutModifyingState (Lean.Meta.withLCtx { fvarIdToDecl := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } } ∅ (Lean.Elab.Term.withSynthesize do let c ← Lean.Elab.Term.elabTermEnsuringType (Lean.Syntax.getOp (Lean.Syntax.getOp optConfig 0) 3) (some (Lean.mkConst `Lean.Meta.Rewrite.Config)) true true none let a ← liftM (Lean.Meta.instantiateMVars c) Lean.Elab.Tactic.eval✝ a))
Equations
- Lean.Elab.Tactic.evalRewriteSeq stx = do let cfg ← liftM (Lean.Elab.Tactic.elabRewriteConfig (Lean.Syntax.getOp stx 1)) let loc : Lean.Elab.Tactic.Location := Lean.Elab.Tactic.expandOptLocation (Lean.Syntax.getOp stx 3) Lean.Elab.Tactic.withRWRulesSeq (Lean.Syntax.getOp stx 0) (Lean.Syntax.getOp stx 2) fun symm term => Lean.Elab.Tactic.withLocation loc (fun a => Lean.Elab.Tactic.rewriteLocalDecl term symm a cfg) (Lean.Elab.Tactic.rewriteTarget term symm cfg) fun a => liftM (Lean.Meta.throwTacticEx `rewrite a (Function.comp Lean.MessageData.ofFormat Lean.format "did not find instance of the pattern in the current goal") Lean.Syntax.missing)