@leanprover/infoview
    Preparing search index...

    Type Alias RpcPtr<T>

    RpcPtr: { __rpcref: string; "[tag]": T } | { "[tag]": T; p: string }

    An RPC pointer is a reference to an object on the lean server. An example where you need this is passing the Environment object, which we need to be able to reference but which would be too large to send over directly.

    Type Parameters

    • T