Documentation

Lean.Meta.Offset

source
def Lean.Meta.isNatProjInst (declName : Lake.Name) (numArgs : Nat) :
Bool
Instances For
    source
    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.

    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
    Instances For