(declare_extra_instruction {Identifier} [T0 = TYPE] ... [TN = TYPE])
Declares an external instruction {Identifier}
with parameters of type [T0]
… [TN]
.
(declare_extra_computation [R = TYPE] {Identifier} [T0 = TYPE] ... [TN = TYPE])
Declares an external computation {Identifier}
with parameters of type [T0]
… [TN]
and returning a value of type [R]
.
(declare_extra_type {Identifier})
Declares an external type.