Documentation

Lean.Meta.Offset

source
def Lean.Meta.isNatProjInst (declName : Lean.Name) (numArgs : Nat) :
Bool
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Meta.evalNat:
Lean.Expr → OptionT Lean.MetaM Nat

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

source
partial def Lean.Meta.evalNat.visit (e : Lean.Expr) :
OptionT Lean.MetaM Nat
source
def Lean.Meta.isDefEqOffset (s : Lean.Expr) (t : Lean.Expr) :
Lean.MetaM Lean.LBool
Equations
  • One or more equations did not get rendered due to their size.