opaque Lean.Meta.Grind.homoExt : Sym.Simp.SymSimpExtension

Extension backing the @[grind homo] attribute.

def Lean.Meta.Grind.getHomoTheorems : CoreM Sym.Simp.Theorems

Returns the homomorphism rules tagged with the [grind hom] attribute.

Equations

• Lean.Meta.Grind.getHomoTheorems = Lean.Meta.Grind.homoExt.getTheorems

opaque Lean.Meta.Grind.homoSourceTypesExt : SimpleScopedEnvExtension Name NameSet

Extension collecting the homomorphism source types: the head constants F of the types τ = F … for which a [grind hom] rule translates Eq τ. The engine marks terms of these types as solver terms so that the E-graph reports their equalities and disequalities (see SolverExtension.markTerm).

def Lean.Meta.Grind.getHomoSourceTypes : CoreM NameSet

Returns the head constants of the homomorphism source types.

Equations

• Lean.Meta.Grind.getHomoSourceTypes = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.Grind.homoSourceTypesExt __do_lift)

def Lean.Meta.Grind.validateHomoTheorem (declName : Name) : MetaM Unit

Ensures a [grind hom] theorem can be applied by Sym.simp without a discharger. Instance-implicit parameters are synthesized during rewriting and need not be determined by the left-hand side. Every other parameter must be inferable from the left-hand side: it must occur in the left-hand side itself (as in (BitVec.cast h a).toNat = a.toNat, where h is instantiated by matching), or in the type of a parameter that does (such parameters are assigned by type unification). A propositional hypothesis failing this test makes the rule conditional: it would have to be discharged when the rule is applied, so the rule would never fire. Any other parameter failing the test cannot be instantiated at all (e.g. it occurs only in the right-hand side).

Equations

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

def Lean.Meta.Grind.addHomoAttr (declName : Name) (attrKind : AttributeKind) : MetaM Unit

Validates and registers a [grind hom] theorem, recording the source type of =-injection rules. See validateHomoTheorem.

Equations

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

structure Lean.Meta.Grind.HomoPredTheorem : Type

A theorem tagged with the [grind hom_pred] attribute.

• declName : Name

  Name of the theorem.

• arity : Nat

  Number of explicit parameters. The theorem is instantiated with the trailing arity arguments of the triggering application.

@[instance_reducible]

instance Lean.Meta.Grind.instInhabitedHomoPredTheorem : Inhabited HomoPredTheorem

Equations

• Lean.Meta.Grind.instInhabitedHomoPredTheorem = { default := Lean.Meta.Grind.instInhabitedHomoPredTheorem.default }

@[instance_reducible]

instance Lean.Meta.Grind.instBEqHomoPredTheorem : BEq HomoPredTheorem

Equations

• Lean.Meta.Grind.instBEqHomoPredTheorem = { beq := Lean.Meta.Grind.instBEqHomoPredTheorem.beq }

def Lean.Meta.Grind.instBEqHomoPredTheorem.beq : HomoPredTheorem → HomoPredTheorem → Bool

Equations

• Lean.Meta.Grind.instBEqHomoPredTheorem.beq { declName := a, arity := a_1 } { declName := b, arity := b_1 } = (a == b && a_1 == b_1)
• Lean.Meta.Grind.instBEqHomoPredTheorem.beq x✝¹ x✝ = false

@[reducible, inline]

abbrev Lean.Meta.Grind.HomoPredTheorems : Type

Map from trigger head symbol to the [grind hom_pred] theorems it activates.

Equations

• Lean.Meta.Grind.HomoPredTheorems = Lean.NameMap (List Lean.Meta.Grind.HomoPredTheorem)

opaque Lean.Meta.Grind.homoPredExt : SimpleScopedEnvExtension (Name × HomoPredTheorem) HomoPredTheorems

Extension backing the @[grind homo_pred] attribute.

def Lean.Meta.Grind.getHomoPredTheorems : CoreM HomoPredTheorems

Returns the homomorphism predicates tagged with the [grind hom_pred] attribute.

Equations

• Lean.Meta.Grind.getHomoPredTheorems = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.Grind.homoPredExt __do_lift)

def Lean.Meta.Grind.addHomoPredAttr (declName : Name) (attrKind : AttributeKind) : MetaM Unit

Validates and registers a [grind hom_pred] theorem. The conclusion of the theorem must contain an application whose trailing arguments are exactly the theorem's explicit parameters. The head symbol of this application is the trigger for the theorem.

Equations

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

def Lean.Meta.Grind.mkHomoPredInstances (e : Expr) : MetaM (Array (Expr × Expr))

Returns the instances of the [grind hom_pred] theorems triggered by e. Each instance is a pair (proof, prop) where proof : prop. A registered theorem whose trigger matches e's head symbol is instantiated with e's trailing arguments; instantiations that fail to elaborate (e.g. because the argument types do not match) are discarded.

Equations

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