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

Equations

• Lean.markBorrowed e = Lean.mkAnnotation (Lean.Name.mkStr1 "borrowed") e

@[export lean_is_marked_borrowed]

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

Equations

• Lean.isMarkedBorrowed e = Option.isSome (Lean.annotation? (Lean.Name.mkStr1 "borrowed") e)