source
opaque Lean.Meta.tactic.hygienic :
Lean.Option Bool
source
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.

Instances For

source
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.

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
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 __discr ← mvarId.introN 1 [name] match __discr with | (fvarIds, mvarId) => pure (fvarIds[0]!, mvarId)

Instances For

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

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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
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.

source
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

Instances For