Function getInteractiveTermGoal

getInteractiveTermGoal(
    rs: RpcSessionAtPos,
    pos: TextDocumentPositionParams,
    options?: ClientRequestOptions,
): Promise<InteractiveTermGoal | undefined>
Parameters
- rs: RpcSessionAtPos
- pos: TextDocumentPositionParams
- Optionaloptions: ClientRequestOptions
Returns Promise<InteractiveTermGoal | undefined>
- Defined in lean4-infoview-api/dist/rpcApi.d.ts:76