Equations
- Lean.Elab.Tactic.evalSplit stx = let _do_jp := fun y => let loc := Lean.Elab.Tactic.expandOptLocation (Lean.Syntax.getOp stx 2); match loc with | Lean.Elab.Tactic.Location.targets hyps simplifyTarget => let _do_jp := fun y => if simplifyTarget = true then Lean.Elab.Tactic.liftMetaTactic fun mvarId => do let discr ← Lean.Meta.splitTarget? mvarId match discr with | some mvarIds => pure mvarIds | x => Lean.throwError (Lean.toMessageData "'split' tactic failed") else do let fvarId ← Lean.Elab.Tactic.getFVarId (Array.getOp hyps 0) Lean.Elab.Tactic.liftMetaTactic fun mvarId => do let discr ← Lean.Meta.splitLocalDecl? mvarId fvarId match discr with | some mvarIds => pure mvarIds | x => Lean.throwError (Lean.toMessageData "'split' tactic failed"); if (decide (Array.size hyps > 0) && simplifyTarget || decide (Array.size hyps > 1)) = true then do let y ← Lean.throwErrorAt (Lean.Syntax.getOp stx 2) (Lean.toMessageData "'split' tactic failed, select a single target to split") _do_jp y else do let y ← pure PUnit.unit _do_jp y | Lean.Elab.Tactic.Location.wildcard => Lean.Elab.Tactic.liftMetaTactic fun mvarId => do let fvarIds ← Lean.Meta.getNondepPropHyps mvarId let r ← forIn fvarIds { fst := none, snd := PUnit.unit } fun fvarId r => let r := r.snd; do let a ← Lean.Meta.splitLocalDecl? mvarId fvarId match a with | some mvarIds => pure (ForInStep.done { fst := some mvarIds, snd := PUnit.unit }) | x => do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → Lean.MetaM (List Lean.MVarId) := fun y => do let discr ← Lean.Meta.splitTarget? mvarId match discr with | some mvarIds => pure mvarIds | x => Lean.throwError (Lean.toMessageData "'split' tactic failed") match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a; if Lean.Syntax.isNone (Lean.Syntax.getOp stx 1) = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "'split' tactic, term to split is not supported yet") _do_jp y