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.

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.

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).

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.

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

@[instance_reducible]

instance Lean.Meta.Grind.instBEqHomoPredTheorem : BEq HomoPredTheorem

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

@[reducible, inline]

abbrev Lean.Meta.Grind.HomoPredTheorems : Type

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

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.

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.

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.