Documentation

Lean.Compiler.BorrowedAnnotation

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