Documentation

Lean.Meta.Offset

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
partial def Lean.Meta.evalNat.evalPow (b n : Expr) :
OptionT MetaM Nat
source
partial def Lean.Meta.evalNat.visit (e : Expr) :
OptionT MetaM 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
    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
        Instances For