opaque Lean.Meta.tactic.hygienic : Lean.Option Bool

def Lean.Meta.mkFreshBinderNameForTacticCore (lctx : LocalContext) (binderName : Name) (hygienic : Bool := true) : MetaM Name

Like mkFreshBinderNameForTactic, but takes the local context and tactic.hygienic value explicitly. Use this variant when the relevant local context is being built incrementally and differs from the ambient ← getLCtx (e.g. when introducing several binders in a single pass).

Equations

• Lean.Meta.mkFreshBinderNameForTacticCore lctx binderName hygienic = if hygienic = true then liftM (Lean.mkFreshUserName binderName) else pure (lctx.getUnusedName binderName)

def Lean.Meta.mkFreshBinderNameForTactic (binderName : Name) : MetaM Name

Similar to Lean.Core.mkFreshUserName, but takes into account the tactic.hygienic option value. If tactic.hygienic = true, then fresh macro scopes are applied to binderName. If not, then returns an (accessible) name based on binderName that is unused in the local context.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.introNCore (mvarId : MVarId) (n : Nat) (givenNames : List Name) (useNamesForExplicitOnly preserveBinderNames : Bool) : MetaM (Array FVarId × MVarId)

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Lean.MVarId.introN (mvarId : MVarId) (n : Nat) (givenNames : List Name := []) (useNamesForExplicitOnly : Bool := false) : MetaM (Array FVarId × MVarId)

Introduce n binders in the goal mvarId.

Equations

• mvarId.introN n givenNames useNamesForExplicitOnly = Lean.Meta.introNCore mvarId n givenNames useNamesForExplicitOnly false

@[reducible, inline]

abbrev Lean.MVarId.introNP (mvarId : MVarId) (n : Nat) : MetaM (Array FVarId × MVarId)

Introduce n binders in the goal mvarId. The new hypotheses are named using the binder names. The suffix P stands for "preserving`.

Equations

• mvarId.introNP n = Lean.Meta.introNCore mvarId n [] false true

def Lean.MVarId.intro (mvarId : MVarId) (name : Name) : MetaM (FVarId × MVarId)

Introduce one binder using name as the new hypothesis name.

Equations

• mvarId.intro name = do let __x ← mvarId.introN 1 [name] match __x with | (fvarIds, mvarId) => pure (fvarIds[0]!, mvarId)

def Lean.Meta.intro1Core (mvarId : MVarId) (preserveBinderNames : Bool) : MetaM (FVarId × MVarId)

Equations

• Lean.Meta.intro1Core mvarId preserveBinderNames = do let __x ← Lean.Meta.introNCore mvarId 1 [] false preserveBinderNames match __x with | (fvarIds, mvarId) => pure (fvarIds[0]!, mvarId)

@[reducible, inline]

abbrev Lean.MVarId.intro1 (mvarId : MVarId) : MetaM (FVarId × MVarId)

Introduce one object from the goal mvarid, without preserving the name used in the binder. Returns a pair made of the newly introduced variable (which will have an inaccessible name) and the new goal. This will fail if there is nothing to introduce, ie when the goal does not start with a forall, lambda or let.

Equations

• mvarId.intro1 = Lean.Meta.intro1Core mvarId false

@[reducible, inline]

abbrev Lean.MVarId.intro1P (mvarId : MVarId) : MetaM (FVarId × MVarId)

Introduce one object from the goal mvarid, preserving the name used in the binder. Returns a pair made of the newly introduced variable and the new goal. This will fail if there is nothing to introduce, ie when the goal does not start with a forall, lambda or let.

Equations

• mvarId.intro1P = Lean.Meta.intro1Core mvarId true

def Lean.MVarId.intro1_ (mvarId : MVarId) : MetaM MVarId

Given a goal ... |- β → α, returns a goal ... ⊢ α. Like intro h; clear h, but without ever appending to the local context.

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Meta.getIntrosSize : Expr → Nat

Calculate the number of new hypotheses that would be created by intros, i.e. the number of binders which can be introduced without unfolding definitions.

def Lean.MVarId.intros (mvarId : MVarId) : MetaM (Array FVarId × MVarId)

Introduce as many binders as possible without unfolding definitions.

Equations

• mvarId.intros = do let type ← mvarId.getType let type ← Lean.instantiateMVars type have n : Nat := Lean.Meta.getIntrosSize type if (n == 0) = true then pure (#[], mvarId) else mvarId.introN n