def Lean.Grind.genPattern {α : Sort u} (_h : Prop) (x _val : α) : α

Gadget for representing generalization steps h : x = val in patterns This gadget is used to represent patterns in theorems that have been generalized to reduce the number of casts introduced during E-matching based instantiation.

For example, consider the theorem

Option.pbind_some {α1 : Type u_1} {a : α1} {α2 : Type u_2}
    {f : (a_1 : α1) → some a = some a_1 → Option α2}
    : (some a).pbind f = f a rfl

Now, suppose we have a goal containing the term c.pbind g and the equivalence class {c, some b}. The E-matching module generates the instance

(some b).pbind (cast ⋯ g)

The cast is necessary because g's type contains c instead of some b. This cast` problematic because we don't have a systematic way of pushing casts over functions to its arguments. Moreover, heterogeneous equality is not effective because the following theorem is not provable in DTT:

theorem hcongr (h₁ : f ≍ g) (h₂ : a ≍ b)  : f a ≍ g b := ...

The standard solution is to generalize the theorem above and write it as

theorem Option.pbind_some'
        {α1 : Type u_1} {a : α1} {α2 : Type u_2}
        {x : Option α1}
        {f : (a_1 : α1) → x = some a_1 → Option α2}
        (h : x = some a)
        : x.pbind f = f a h := by
  subst h
  apply Option.pbind_some

Internally, we use this gadget to mark the E-matching pattern as

(genPattern h x (some a)).pbind f

This pattern is matched in the same way we match (some a).pbind f, but it saves the proof for the actual term to the some-application in f, and the actual term in x.

In the example above, c.pbind g also matches the pattern (genPattern h x (some a)).pbind f, and stores c in x, b in a, and the proof that c = some b in h.

Equations

• Lean.Grind.genPattern _h x _val = x

def Lean.Grind.genHEqPattern {α β : Sort u} (_h : Prop) (x : α) (_val : β) : α

Similar to genPattern but for the heterogeneous case

Equations

• Lean.Grind.genHEqPattern _h x _val = x

def Lean.Parser.resetGrindAttrs : ParserDescr

Reset all grind attributes. This command is intended for testing purposes only and should not be used in applications.

Equations

• Lean.Parser.resetGrindAttrs = Lean.ParserDescr.node `Lean.Parser.resetGrindAttrs 1024 (Lean.ParserDescr.symbol "reset_grind_attrs%")

def Lean.Parser.Attr.grindGen : ParserDescr

Equations

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

def Lean.Parser.Attr.grindEq : ParserDescr

Equations

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

def Lean.Parser.Attr.grindEqBoth : ParserDescr

Equations

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

def Lean.Parser.Attr.grindEqRhs : ParserDescr

Equations

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

def Lean.Parser.Attr.grindEqBwd : ParserDescr

Equations

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

def Lean.Parser.Attr.grindBwd : ParserDescr

Equations

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

def Lean.Parser.Attr.grindFwd : ParserDescr

Equations

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

def Lean.Parser.Attr.grindRL : ParserDescr

Equations

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

def Lean.Parser.Attr.grindLR : ParserDescr

Equations

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

def Lean.Parser.Attr.grindUsr : ParserDescr

Equations

• Lean.Parser.Attr.grindUsr = Lean.ParserDescr.nodeWithAntiquot "grindUsr" `Lean.Parser.Attr.grindUsr (Lean.ParserDescr.nonReservedSymbol "usr" false)

def Lean.Parser.Attr.grindCases : ParserDescr

Equations

• Lean.Parser.Attr.grindCases = Lean.ParserDescr.nodeWithAntiquot "grindCases" `Lean.Parser.Attr.grindCases (Lean.ParserDescr.nonReservedSymbol "cases" false)

def Lean.Parser.Attr.grindCasesEager : ParserDescr

Equations

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

def Lean.Parser.Attr.grindIntro : ParserDescr

Equations

• Lean.Parser.Attr.grindIntro = Lean.ParserDescr.nodeWithAntiquot "grindIntro" `Lean.Parser.Attr.grindIntro (Lean.ParserDescr.nonReservedSymbol "intro" false)

def Lean.Parser.Attr.grindExt : ParserDescr

Equations

• Lean.Parser.Attr.grindExt = Lean.ParserDescr.nodeWithAntiquot "grindExt" `Lean.Parser.Attr.grindExt (Lean.ParserDescr.nonReservedSymbol "ext" false)

def Lean.Parser.Attr.grindSym : ParserDescr

Equations

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

def Lean.Parser.Attr.grindMod : ParserDescr

Equations

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

def Lean.Parser.Attr.grind : ParserDescr

Equations

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

def Lean.Parser.Attr.grind? : ParserDescr

Equations

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