Equations
- Lean.Meta.constructor mvarId = Lean.Meta.withMVarContext mvarId do Lean.Meta.checkNotAssigned mvarId `constructor let target ← Lean.Meta.getMVarType' mvarId Lean.matchConstInduct (Lean.Expr.getAppFn target) (fun x => Lean.Meta.throwTacticEx `constructor mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "target is not an inductive datatype") Lean.Syntax.missing) fun ival us => do let r ← let col := ival.ctors; forIn col { fst := none, snd := PUnit.unit } fun ctor r => let r := r.snd; do let r ← tryCatch (do let a ← Lean.Meta.apply mvarId (Lean.mkConst ctor us) pure (DoResultPR.return a PUnit.unit)) fun x => do let y ← pure () pure (DoResultPR.pure y PUnit.unit) match r with | DoResultPR.pure a u => let x := u; do pure a pure (ForInStep.yield { fst := none, snd := PUnit.unit }) | DoResultPR.return b u => let x := u; pure (ForInStep.done { fst := some b, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → Lean.MetaM (List Lean.MVarId) := fun y => Lean.Meta.throwTacticEx `constructor mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "no applicable constructor found") Lean.Syntax.missing match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a
Equations
- Lean.Meta.existsIntro mvarId w = Lean.Meta.withMVarContext mvarId do Lean.Meta.checkNotAssigned mvarId `exists let target ← Lean.Meta.getMVarType' mvarId Lean.matchConstStruct (Lean.Expr.getAppFn target) (fun x => Lean.Meta.throwTacticEx `exists mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "target is not an inductive datatype with one constructor") Lean.Syntax.missing) fun ival us cval => let _do_jp := fun y => let ctor := Lean.mkAppN (Lean.mkConst cval.toConstantVal.name us) (Array.ofSubarray (Array.toSubarray (Lean.Expr.getAppArgs target) 0 cval.numParams)); do let ctorType ← Lean.Meta.inferType ctor let discr ← Lean.Meta.forallMetaTelescopeReducing ctorType (some (cval.numFields - 2)) Lean.MetavarKind.natural let x : Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr := discr match x with | (mvars, x, x_1) => let f := Lean.mkAppN ctor mvars; do Lean.Meta.checkApp f w let discr ← Lean.Meta.apply mvarId (Lean.mkApp f w) match discr with | [mvarId] => pure mvarId | x => Lean.Meta.throwTacticEx `exists mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "unexpected number of subgoals") Lean.Syntax.missing; if cval.numFields < 2 then do let y ← Lean.Meta.throwTacticEx `exists mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "constructor must have at least two fields") Lean.Syntax.missing _do_jp y else do let y ← pure PUnit.unit _do_jp y