Documentation

Lean.Meta.Tactic.Intro

constant Lean.Meta.tactic.hygienic :

Lean.Option Bool

def Lean.Meta.getHygienicIntro :

Lean.MetaM Bool

Equations

Lean.Meta.getHygienicIntro = do let a ← Lean.getOptions pure (Lean.Option.get a Lean.Meta.tactic.hygienic)

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

Lean.Meta.introNCore mvarId n givenNames useNamesForExplicitOnly preserveBinderNames = do let hygienic ← Lean.Meta.getHygienicIntro if (n == 0) = true then pure (#[], mvarId) else Lean.Meta.introNImp mvarId n (Lean.Meta.mkAuxNameImp preserveBinderNames hygienic useNamesForExplicitOnly) givenNames

@[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 let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (fvarIds, mvarId) => pure (Array.get! fvarIds 0, mvarId)

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

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

Equations

Lean.Meta.intro1Core mvarId preserveBinderNames = do let discr ← Lean.Meta.introNCore mvarId 1 [] false preserveBinderNames let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (fvarIds, mvarId) => pure (Array.get! fvarIds 0, mvarId)

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

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