Extensions 

(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.