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

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

source
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))

Instances For

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

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

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

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

Instances For