partial def Lean.Meta.evalNat (e : Lean.Expr) : OptionT Lean.MetaM Nat

Evaluate simple Nat expressions. Remark: this method assumes the given expression has type Nat.

partial def Lean.Meta.evalNat.evalPow (b n : Lean.Expr) : OptionT Lean.MetaM Nat

partial def Lean.Meta.evalNat.visit (e : Lean.Expr) : OptionT Lean.MetaM Nat

def Lean.Meta.matchesInstance (e inst : Lean.Expr) : Lean.MetaM Bool

Checks that expression e is definitional equal to inst.

Uses instances transparency so that reducible terms and instances extended other instances are unfolded.

Equations

• Lean.Meta.matchesInstance e inst = Lean.Meta.withNewMCtxDepth (Lean.Meta.withTransparency Lean.Meta.TransparencyMode.instances (Lean.Meta.isDefEq e inst))

partial def Lean.Meta.isOffset? (e : Lean.Expr) : OptionT Lean.MetaM (Lean.Expr × Nat)

Similar to getOffset but returns none if the expression is not an offset.

def Lean.Meta.isDefEqOffset (s t : Lean.Expr) : Lean.MetaM Lean.LBool