inductive Lean.Meta.Grind.Origin : Type

• decl (declName : Lean.Name) : Lean.Meta.Grind.Origin

  A global declaration in the environment.

• fvar (fvarId : Lean.FVarId) : Lean.Meta.Grind.Origin

  A local hypothesis.

• stx (id : Lean.Name) (ref : Lean.Syntax) : Lean.Meta.Grind.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 : Lean.Meta.Grind.Origin

Instances For

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

instance Lean.Meta.Grind.instInhabitedOrigin : Inhabited Lean.Meta.Grind.Origin

Equations

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

instance Lean.Meta.Grind.instReprOrigin : Repr Lean.Meta.Grind.Origin

Equations

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

def Lean.Meta.Grind.Origin.key : Lean.Meta.Grind.Origin → Lean.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] [Lean.MonadEnv m] [Lean.MonadError m] (o : Lean.Meta.Grind.Origin) : m Lean.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 Lean.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 : Lean.Expr
• numParams : Nat
• patterns : List Lean.Expr
• symbols : List Lean.HeadIndex

  Contains all symbols used in pattterns.

• origin : Lean.Meta.Grind.Origin

Instances For

• Lean.Meta.Grind.instInhabitedEMatchTheorem

instance Lean.Meta.Grind.instInhabitedEMatchTheorem : Inhabited Lean.Meta.Grind.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 : Lean.Meta.Grind.EMatchTheorems) (thm : Lean.Meta.Grind.EMatchTheorem) : Lean.Meta.Grind.EMatchTheorems

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

• symbols : Array Lean.HeadIndex
• symbolSet : Std.HashSet Lean.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 Lean.Expr) : Lean.MetaM (List Lean.Expr × List Lean.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 : Lean.Meta.Grind.CheckCoverageResult

  checkCoverage succeeded

• missing (pos : List Nat) : Lean.Meta.Grind.CheckCoverageResult

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

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

Equations

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

def Lean.Meta.Grind.getEMatchTheorems : Lean.CoreM Lean.Meta.Grind.EMatchTheorems

Equations

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