def Lean.Expr.ctorWeight : Lean.Expr → UInt8

Equations

• (Lean.Expr.bvar deBruijnIndex).ctorWeight = 0
• (Lean.Expr.fvar fvarId).ctorWeight = 1
• (Lean.Expr.mvar mvarId).ctorWeight = 2
• (Lean.Expr.sort u).ctorWeight = 3
• (Lean.Expr.const declName us).ctorWeight = 4
• (Lean.Expr.lit a).ctorWeight = 5
• (Lean.Expr.mdata data expr).ctorWeight = 6
• (Lean.Expr.proj typeName idx struct).ctorWeight = 7
• (fn.app arg).ctorWeight = 8
• (Lean.Expr.lam binderName binderType body binderInfo).ctorWeight = 9
• (Lean.Expr.forallE binderName binderType body binderInfo).ctorWeight = 10
• (Lean.Expr.letE declName type value body nonDep).ctorWeight = 11

inductive Lean.Meta.ACLt.ReduceMode : Type

• reduce: Lean.Meta.ACLt.ReduceMode
• reduceSimpleOnly: Lean.Meta.ACLt.ReduceMode
• none: Lean.Meta.ACLt.ReduceMode

def Lean.Meta.ACLt.main (a : Lean.Expr) (b : Lean.Expr) (mode : optParam Lean.Meta.ACLt.ReduceMode Lean.Meta.ACLt.ReduceMode.none) : Lean.MetaM Bool

An AC-compatible ordering.

Recall that an AC-compatible ordering if it is monotonic, well-founded, and total. Both KBO and LPO are AC-compatible. KBO is faster, but we do not cache the weight of each expression in Lean 4. Even if we did, we would need to have a weight where implicit instance arguments are ignored. So, we use a LPO-like term ordering.

Remark: this method is used to implement ordered rewriting. We ignore implicit instance arguments to address an issue reported at issue #972.

Remark: the order is not really total on terms since

• We instance implicit arguments.
• We ignore metadata.
• We ignore universe parameterst at constants.

Equations

• Lean.Meta.ACLt.main a b mode = Lean.Meta.ACLt.main.lt mode a b

def Lean.Meta.ACLt.main.reduce (mode : optParam Lean.Meta.ACLt.ReduceMode Lean.Meta.ACLt.ReduceMode.none) (e : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.ACLt.main.reduce Lean.Meta.ACLt.ReduceMode.none e = if e.hasLooseBVars = true then pure e else pure e

partial def Lean.Meta.ACLt.main.lt (mode : optParam Lean.Meta.ACLt.ReduceMode Lean.Meta.ACLt.ReduceMode.none) (a : Lean.Expr) (b : Lean.Expr) : Lean.MetaM Bool

partial def Lean.Meta.ACLt.main.ltPair (mode : optParam Lean.Meta.ACLt.ReduceMode Lean.Meta.ACLt.ReduceMode.none) (a₁ : Lean.Expr) (a₂ : Lean.Expr) (b₁ : Lean.Expr) (b₂ : Lean.Expr) : Lean.MetaM Bool

def Lean.Meta.ACLt.main.getParamsInfo (f : Lean.Expr) (numArgs : Nat) : Lean.MetaM (Array Lean.Meta.ParamInfo)

Equations

• Lean.Meta.ACLt.main.getParamsInfo f numArgs = if f.hasLooseBVars = true then pure #[] else do let __do_lift ← Lean.Meta.getFunInfoNArgs f numArgs pure __do_lift.paramInfo

partial def Lean.Meta.ACLt.main.ltApp (mode : optParam Lean.Meta.ACLt.ReduceMode Lean.Meta.ACLt.ReduceMode.none) (a : Lean.Expr) (b : Lean.Expr) : Lean.MetaM Bool

partial def Lean.Meta.ACLt.main.lexSameCtor (mode : optParam Lean.Meta.ACLt.ReduceMode Lean.Meta.ACLt.ReduceMode.none) (a : Lean.Expr) (b : Lean.Expr) : Lean.MetaM Bool

partial def Lean.Meta.ACLt.main.allChildrenLt (mode : optParam Lean.Meta.ACLt.ReduceMode Lean.Meta.ACLt.ReduceMode.none) (a : Lean.Expr) (b : Lean.Expr) : Lean.MetaM Bool

partial def Lean.Meta.ACLt.main.someChildGe (mode : optParam Lean.Meta.ACLt.ReduceMode Lean.Meta.ACLt.ReduceMode.none) (a : Lean.Expr) (b : Lean.Expr) : Lean.MetaM Bool

partial def Lean.Meta.ACLt.main.lpo (mode : optParam Lean.Meta.ACLt.ReduceMode Lean.Meta.ACLt.ReduceMode.none) (a : Lean.Expr) (b : Lean.Expr) : Lean.MetaM Bool

def Lean.Meta.acLt (a : Lean.Expr) (b : Lean.Expr) (mode : optParam Lean.Meta.ACLt.ReduceMode Lean.Meta.ACLt.ReduceMode.none) : Lean.MetaM Bool

An AC-compatible ordering.

Recall that an AC-compatible ordering if it is monotonic, well-founded, and total. Both KBO and LPO are AC-compatible. KBO is faster, but we do not cache the weight of each expression in Lean 4. Even if we did, we would need to have a weight where implicit instance arguments are ignored. So, we use a LPO-like term ordering.

Remark: this method is used to implement ordered rewriting. We ignore implicit instance arguments to address an issue reported at issue #972.

Remark: the order is not really total on terms since

• We instance implicit arguments.
• We ignore metadata.
• We ignore universe parameterst at constants.

Equations

• Lean.Meta.acLt a b mode = Lean.Meta.ACLt.main a b mode