Lean.Meta.Tactic.Util

source

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

Lean.MetaM Lean.Name

Equations

Lean.Meta.getMVarTag mvarId = do let a ← Lean.Meta.getMVarDecl mvarId pure a.userName

source

def Lean.Meta.setMVarTag (mvarId : Lean.MVarId) (tag : Lean.Name) :

Lean.MetaM Unit

Equations

Lean.Meta.setMVarTag mvarId tag = modify fun s => { mctx := Lean.MetavarContext.renameMVar s.mctx mvarId tag, cache := s.cache, zetaFVarIds := s.zetaFVarIds, postponed := s.postponed }

source

def Lean.Meta.appendTag (tag : Lean.Name) (suffix : Lean.Name) :

Lean.Name

Equations

Lean.Meta.appendTag tag suffix = Lean.Name.modifyBase tag fun a => a ++ Lean.Name.eraseMacroScopes suffix

source

def Lean.Meta.appendTagSuffix (mvarId : Lean.MVarId) (suffix : Lean.Name) :

Lean.MetaM Unit

Equations

Lean.Meta.appendTagSuffix mvarId suffix = do let tag ← Lean.Meta.getMVarTag mvarId Lean.Meta.setMVarTag mvarId (Lean.Meta.appendTag tag suffix)

source

def Lean.Meta.mkFreshExprSyntheticOpaqueMVar (type : Lean.Expr) (tag : optParam Lean.Name Lean.Name.anonymous) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkFreshExprSyntheticOpaqueMVar type tag = Lean.Meta.mkFreshExprMVar (some type) Lean.MetavarKind.syntheticOpaque tag

source

def Lean.Meta.throwTacticEx {α : Type} (tacticName : Lean.Name) (mvarId : Lean.MVarId) (msg : Lean.MessageData) (ref : optParam Lean.Syntax Lean.Syntax.missing) :

Lean.MetaM α

Equations

Lean.Meta.throwTacticEx tacticName mvarId msg ref = Lean.throwError (Lean.toMessageData "tactic '" ++ Lean.toMessageData tacticName ++ Lean.toMessageData "' failed, " ++ Lean.toMessageData msg ++ Lean.toMessageData "\n" ++ Lean.toMessageData (Lean.MessageData.ofGoal mvarId) ++ Lean.toMessageData "")

source

def Lean.Meta.throwNestedTacticEx {α : Type} (tacticName : Lean.Name) (ex : Lean.Exception) :

Lean.MetaM α

Equations

Lean.Meta.throwNestedTacticEx tacticName ex = Lean.throwError (Lean.toMessageData "tactic '" ++ Lean.toMessageData tacticName ++ Lean.toMessageData "' failed, nested error:\n" ++ Lean.toMessageData (Lean.Exception.toMessageData ex) ++ Lean.toMessageData "")

source

def Lean.Meta.checkNotAssigned (mvarId : Lean.MVarId) (tacticName : Lean.Name) :

Lean.MetaM Unit

Equations

Lean.Meta.checkNotAssigned mvarId tacticName = do let a ← Lean.Meta.isExprMVarAssigned mvarId if a = true then Lean.Meta.throwTacticEx tacticName mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "metavariable has already been assigned") Lean.Syntax.missing else pure PUnit.unit

source

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

Lean.MetaM Lean.Expr

Equations

Lean.Meta.getMVarType mvarId = do let a ← Lean.Meta.getMVarDecl mvarId pure a.type

source

def Lean.Meta.getMVarType' (mvarId : Lean.MVarId) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.getMVarType' mvarId = do let a ← Lean.Meta.getMVarDecl mvarId let a ← Lean.Meta.instantiateMVars a.type Lean.Meta.whnf a

source

def Lean.Meta.admit (mvarId : Lean.MVarId) (synthetic : optParam Bool true) :

Lean.MetaM Unit

Equations

Lean.Meta.admit mvarId synthetic = Lean.Meta.withMVarContext mvarId do Lean.Meta.checkNotAssigned mvarId `admit let mvarType ← Lean.Meta.getMVarType mvarId let val ← Lean.Meta.mkSorry mvarType synthetic Lean.Meta.assignExprMVar mvarId val

source

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

Lean.MetaM Unit

Equations

Lean.Meta.headBetaMVarType mvarId = do let a ← Lean.Meta.getMVarType mvarId Lean.Meta.setMVarType mvarId (Lean.Expr.headBeta a)

source

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

Lean.MetaM (Array Lean.FVarId)

Equations

Lean.Meta.getNondepPropHyps mvarId = (fun removeDeps => Lean.Meta.withMVarContext mvarId (let candidates := ∅; do let a ← Lean.getLCtx let r ← let col := a; forIn col candidates fun localDecl r => let candidates := r; if Lean.LocalDecl.isAuxDecl localDecl = true then do pure PUnit.unit pure (ForInStep.yield candidates) else do let r ← removeDeps (Lean.LocalDecl.type localDecl) candidates let candidates : Lean.FVarIdHashSet := r let _do_jp : Lean.FVarIdHashSet → Unit → Lean.MetaM (ForInStep Lean.FVarIdHashSet) := fun candidates y => do let a ← Lean.Meta.isProp (Lean.LocalDecl.type localDecl) if (a && !Lean.LocalDecl.hasValue localDecl) = true then let candidates := Std.HashSet.insert candidates (Lean.LocalDecl.fvarId localDecl); do pure PUnit.unit pure (ForInStep.yield candidates) else do pure PUnit.unit pure (ForInStep.yield candidates) match Lean.LocalDecl.value? localDecl with | none => do let y ← pure () _do_jp candidates y | some value => do let r ← removeDeps value candidates let candidates : Lean.FVarIdHashSet := r let y ← pure PUnit.unit _do_jp candidates y let x : Lean.FVarIdHashSet := r let candidates : Lean.FVarIdHashSet := x let a ← Lean.Meta.getMVarType mvarId let r ← removeDeps a candidates let candidates : Lean.FVarIdHashSet := r if Std.HashSet.isEmpty candidates = true then pure #[] else let result := #[]; do let a ← Lean.getLCtx let r ← let col := a; forIn col result fun localDecl r => let result := r; if Std.HashSet.contains candidates (Lean.LocalDecl.fvarId localDecl) = true then let result := Array.push result (Lean.LocalDecl.fvarId localDecl); do pure PUnit.unit pure (ForInStep.yield result) else do pure PUnit.unit pure (ForInStep.yield result) let x : Array Lean.FVarId := r let result : Array Lean.FVarId := x pure result)) Lean.Meta.getNondepPropHyps.removeDeps

source

def Lean.Meta.getNondepPropHyps.removeDeps (e : Lean.Expr) (candidates : Lean.FVarIdHashSet) :

Lean.MetaM Lean.FVarIdHashSet

Equations

Lean.Meta.getNondepPropHyps.removeDeps e candidates = do let e ← Lean.Meta.instantiateMVars e let visit : StateRefT' IO.RealWorld Lean.FVarIdHashSet Lean.MetaM Lean.FVarIdHashSet := do Lean.Expr.forEach e fun x => match x with | Lean.Expr.fvar fvarId x => modify fun s => Std.HashSet.erase s fvarId | x => pure () get StateRefT'.run' visit candidates

source

def Lean.Meta.saturate (mvarId : Lean.MVarId) (x : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))) :

Lean.MetaM (List Lean.MVarId)

Equations

Lean.Meta.saturate mvarId x = (fun go => do let discr ← StateRefT'.run (go mvarId) #[] let x : Unit × Array Lean.MVarId := discr match x with | (x, r) => pure (Array.toList r)) (Lean.Meta.saturate.go x)

source

partial def Lean.Meta.saturate.go (x : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))) (mvarId : Lean.MVarId) :

StateRefT' IO.RealWorld (Array Lean.MVarId) Lean.MetaM Unit

source

def Lean.Meta.exactlyOne (mvarIds : List Lean.MVarId) (msg : optParam Lean.MessageData (Function.comp Lean.MessageData.ofFormat Lean.format "unexpected number of goals")) :

Lean.MetaM Lean.MVarId

Equations

Lean.Meta.exactlyOne mvarIds msg = match mvarIds with | [mvarId] => pure mvarId | x => Lean.throwError msg

source

def Lean.Meta.ensureAtMostOne (mvarIds : List Lean.MVarId) (msg : optParam Lean.MessageData (Function.comp Lean.MessageData.ofFormat Lean.format "unexpected number of goals")) :

Lean.MetaM (Option Lean.MVarId)

Equations

Lean.Meta.ensureAtMostOne mvarIds msg = match mvarIds with | [] => pure none | [mvarId] => pure (some mvarId) | x => Lean.throwError msg