$double constructor

$double(
  1. double $value
)

Wrap a double in a $double.

Implementation

$double(super.$value);