Documentation

Lean.Meta.Tactic.Intro

opaque Lean.Meta.tactic.hygienic:

Lean.Option Bool

def Lean.Meta.introNCore (mvarId : Lean.MVarId) (n : Nat) (givenNames : List Lean.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]

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

Lean.MetaM (Array Lean.FVarId × Lean.MVarId)

Equations

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

@[inline]

abbrev Lean.Meta.introNP (mvarId : Lean.MVarId) (n : Nat) :

Lean.MetaM (Array Lean.FVarId × Lean.MVarId)

Equations

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

def Lean.Meta.intro (mvarId : Lean.MVarId) (name : Lean.Name) :

Lean.MetaM (Lean.FVarId × Lean.MVarId)

Equations

Lean.Meta.intro mvarId name = do let discr ← Lean.Meta.introN mvarId 1 [name] false match discr with | (fvarIds, mvarId) => pure (Array.getOp fvarIds 0, mvarId)

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]

abbrev Lean.Meta.intro1 (mvarId : Lean.MVarId) :

Lean.MetaM (Lean.FVarId × Lean.MVarId)

Equations

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

@[inline]

abbrev Lean.Meta.intro1P (mvarId : Lean.MVarId) :

Lean.MetaM (Lean.FVarId × Lean.MVarId)

Equations

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

def Lean.Meta.intros (mvarId : Lean.MVarId) :

Lean.MetaM (Array Lean.FVarId × Lean.MVarId)

Equations

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