def Lean.Expr.ctorWeight : Expr → UInt8

inductive Lean.Meta.ACLt.ReduceMode : Type

• reduce : ReduceMode
• reduceSimpleOnly : ReduceMode
• none : ReduceMode

def Lean.Meta.ACLt.main (a b : Expr) (mode : ReduceMode := ReduceMode.none) : 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.

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

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

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

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

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

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

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

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

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

def Lean.Meta.acLt (a b : Expr) (mode : ACLt.ReduceMode := ACLt.ReduceMode.none) : 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.