Documentation

Lean.Compiler.BorrowedAnnotation

source
def Lean.markBorrowed (e : Lean.Expr) :
Lean.Expr
Equations
source
@[export lean_is_marked_borrowed]
def Lean.isMarkedBorrowed (e : Lean.Expr) :
Bool
Equations