inductive Lean.Meta.Grind.Origin : Type

• decl (declName : Name) : Origin

  A global declaration in the environment.

• fvar (fvarId : FVarId) : Origin

  A local hypothesis.

• stx (id : Name) (ref : Syntax) : Origin

  A proof term provided directly to a call to grind where ref is the provided grind argument. The id is a unique identifier for the call.

• other : Origin

Instances For

• Lean.Meta.Grind.instInhabitedOrigin
• Lean.Meta.Grind.instReprOrigin

instance Lean.Meta.Grind.instInhabitedOrigin : Inhabited Origin

Equations

• Lean.Meta.Grind.instInhabitedOrigin = { default := Lean.Meta.Grind.Origin.decl default }

instance Lean.Meta.Grind.instReprOrigin : Repr Origin

Equations

• Lean.Meta.Grind.instReprOrigin = { reprPrec := Lean.Meta.Grind.reprOrigin✝ }

def Lean.Meta.Grind.Origin.key : Origin → Name

A unique identifier corresponding to the origin.

Equations

• (Lean.Meta.Grind.Origin.decl a).key = a
• (Lean.Meta.Grind.Origin.fvar a).key = a.name
• (Lean.Meta.Grind.Origin.stx a a_1).key = a
• Lean.Meta.Grind.Origin.other.key = `other

def Lean.Meta.Grind.Origin.pp {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] (o : Origin) : m MessageData

Equations

• (Lean.Meta.Grind.Origin.decl a).pp = do let __do_lift ← Lean.mkConstWithLevelParams a pure (Lean.MessageData.ofConst __do_lift)
• (Lean.Meta.Grind.Origin.fvar a).pp = pure (Lean.MessageData.ofExpr (Lean.mkFVar a))
• (Lean.Meta.Grind.Origin.stx a a_1).pp = pure (Lean.MessageData.ofSyntax a_1)
• Lean.Meta.Grind.Origin.other.pp = pure ((Lean.MessageData.ofFormat ∘ Std.format) "[unknown]")

structure Lean.Meta.Grind.EMatchTheorem : Type

A theorem for heuristic instantiation based on E-matching.

• levelParams : Array Name

  It stores universe parameter names for universe polymorphic proofs. Recall that it is non-empty only when we elaborate an expression provided by the user. When proof is just a constant, we can use the universe parameter names stored in the declaration.

• proof : Expr
• numParams : Nat
• patterns : List Expr
• symbols : List HeadIndex

  Contains all symbols used in pattterns.

• origin : Origin

Instances For

• Lean.Meta.Grind.instInhabitedEMatchTheorem

instance Lean.Meta.Grind.instInhabitedEMatchTheorem : Inhabited EMatchTheorem

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Grind.EMatchTheorems : Type

The key is a symbol from EMatchTheorem.symbols.

Equations

• Lean.Meta.Grind.EMatchTheorems = Lean.PHashMap Lean.Name (List Lean.Meta.Grind.EMatchTheorem)

def Lean.Meta.Grind.EMatchTheorems.insert (s : EMatchTheorems) (thm : EMatchTheorem) : EMatchTheorems

Equations

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

def Lean.Meta.Grind.EMatchTheorem.getProofWithFreshMVarLevels (thm : EMatchTheorem) : MetaM Expr

Equations

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

def Lean.Meta.Grind.mkGroundPattern (e : Expr) : Expr

Equations

• Lean.Meta.Grind.mkGroundPattern e = Lean.mkAnnotation `grind.ground_pat e

def Lean.Meta.Grind.groundPattern? (e : Expr) : Option Expr

Equations

• Lean.Meta.Grind.groundPattern? e = Lean.annotation? `grind.ground_pat e

def Lean.Meta.Grind.isPatternDontCare (e : Expr) : Bool

Equations

• Lean.Meta.Grind.isPatternDontCare e = (e == Lean.Meta.Grind.dontCare✝)

partial def Lean.Meta.Grind.ppPattern (pattern : Expr) : MessageData

structure Lean.Meta.Grind.NormalizePattern.State : Type

• symbols : Array HeadIndex
• symbolSet : Std.HashSet HeadIndex
• bvarsFound : Std.HashSet Nat

@[reducible, inline]

abbrev Lean.Meta.Grind.NormalizePattern.M (α : Type) : Type

Equations

• Lean.Meta.Grind.NormalizePattern.M = StateRefT' IO.RealWorld Lean.Meta.Grind.NormalizePattern.State Lean.MetaM

def Lean.Meta.Grind.NormalizePattern.main (patterns : List Expr) : MetaM (List Expr × List HeadIndex × Std.HashSet Nat)

Equations

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

inductive Lean.Meta.Grind.CheckCoverageResult : Type

Auxiliary type for the checkCoverage function.

• ok : CheckCoverageResult

  checkCoverage succeeded

• missing (pos : List Nat) : CheckCoverageResult

  checkCoverage failed because some of the theorem parameters are missing, pos contains their positions

def Lean.Meta.Grind.addEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) : MetaM Unit

Equations

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

def Lean.Meta.Grind.getEMatchTheorems : CoreM EMatchTheorems

Equations

• Lean.Meta.Grind.getEMatchTheorems = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.Grind.ematchTheoremsExt✝ __do_lift)