Require Plus.
Extraction NoInline plus_is_one.
Require Addr.
Extraction NoInline ad_double ad_double_plus_un.