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

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

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

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

def Lean.Meta.matchesInstance (e inst : Expr) : 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 : Expr) : OptionT MetaM (Expr × Nat)

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

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

Equations

• One or more equations did not get rendered due to their size.