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

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

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

Equations

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

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

Equations

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

@[inline, reducible]

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

Introduce n binders in the goal mvarId.

Equations

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

@[inline, reducible, deprecated Lean.MVarId.introN]

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

Equations

• Lean.Meta.introN mvarId n givenNames useNamesForExplicitOnly = Lean.MVarId.introN mvarId n givenNames useNamesForExplicitOnly

@[inline, reducible]

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

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

Equations

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

@[inline, reducible, deprecated Lean.MVarId.introNP]

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

Equations

• Lean.Meta.introNP mvarId n = Lean.MVarId.introNP mvarId n

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

Introduce one binder using name as the the new hypothesis name.

Equations

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

@[deprecated Lean.MVarId.intro]

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

Equations

• Lean.Meta.intro mvarId name = Lean.MVarId.intro mvarId name

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

Equations

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

@[inline, reducible]

abbrev Lean.MVarId.intro1 (mvarId : Lean.MVarId) : Lean.MetaM (Lean.FVarId × Lean.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

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

@[inline, reducible, deprecated Lean.MVarId.intro1]

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

Equations

• Lean.Meta.intro1 mvarId = Lean.MVarId.intro1 mvarId

@[inline, reducible]

abbrev Lean.MVarId.intro1P (mvarId : Lean.MVarId) : Lean.MetaM (Lean.FVarId × Lean.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

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

@[inline, reducible, deprecated Lean.MVarId.intro1P]

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

Equations

• Lean.Meta.intro1P mvarId = Lean.MVarId.intro1P mvarId

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

Introduce as many binders as possible without unfolding definitions.

Equations

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

@[deprecated Lean.MVarId.intros]

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

Equations

• Lean.Meta.intros mvarId = Lean.MVarId.intros mvarId