def Lean.markBorrowed (e : Lean.Expr) : Lean.Expr

Equations

• Lean.markBorrowed e = Lean.mkAnnotation `borrowed e

@[export lean_is_marked_borrowed]

def Lean.isMarkedBorrowed (e : Lean.Expr) : Bool

Equations

• Lean.isMarkedBorrowed e = (Lean.annotation? `borrowed e).isSome