ForeignType Pointer -- dereference a pointer

Description

Dereference the given pointer into the corresponding foreign object, much like the dereference operator (*) in C.

i1 : x = int 5

o1 = 5

o1 : ForeignObject of type int32

i2 : ptr = address x

o2 = 0x7f083bcb8c50

o2 : Pointer

i3 : int ptr

o3 = 5

o3 : ForeignObject of type int32

The source of this document is in ForeignFunctions.m2:896:0.