← Mathematical handbook

def Lean.markBorrowed (e : Expr) : Expr

Equations

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

def Lean.isMarkedBorrowed (e : Expr) : Bool

Equations

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