def Lean.Expr.appM? (e : Expr) (fName : Name) : Option (Array Expr)

If e represents an application of a function with the name fname, return the representations of its arguments. Otherwise return none.

Equations

• e.appM? fName = if e.isAppOf fName = true then some e.getAppArgs else none

def Lean.Expr.modifyAppOptM (e : Expr) (args : Array (Option Expr)) : Expr

Modify the arguments of the function application represented by e. If an element in args is none, then the corresponding argument in the function application remains unchanged.

Equations

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

def Lean.Expr.getMDataName? : Expr → Option Name

Get the mdata entry with the key "name", if available.

Equations

• (Lean.Expr.mdata md expr).getMDataName? = Lean.KVMap.get? md `name
• x✝.getMDataName? = none

def Lean.Expr.setMDataName? (e : Expr) (name : Name) : Expr

Set the mdata entry of e with the key "name" to name.

Equations

• (Lean.Expr.mdata md expr).setMDataName? name = Lean.mkMData (Lean.KVMap.insert md `name (Lean.DataValue.ofName name)) expr
• e.setMDataName? name = Lean.mkMData (Lean.KVMap.empty.insert `name (Lean.DataValue.ofName name)) e