Documentation

Lean.Meta.ACLt

source
def Lean.Expr.ctorWeight :
Lean.Expr → UInt8
Equations
  • One or more equations did not get rendered due to their size.
source
inductive Lean.Meta.ACLt.ReduceMode :
Type
Instances For
    source
    unsafe 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 instace 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
    source
    unsafe 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.
    source
    unsafe 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
    Equations
    • One or more equations did not get rendered due to their size.
    source
    unsafe 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
    Equations
    • One or more equations did not get rendered due to their size.
    source
    unsafe 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
    Equations
    • One or more equations did not get rendered due to their size.
    source
    unsafe 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
    Equations
    • One or more equations did not get rendered due to their size.
    source
    unsafe 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
    Equations
    • One or more equations did not get rendered due to their size.
    source
    unsafe 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
    Equations
    source
    unsafe 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
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[implemented_by Lean.Meta.ACLt.main]
    opaque Lean.Meta.Expr.acLt :
    Lean.Expr → Lean.Expr → 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 instace 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.