new_binder

boolSyntax.new_binder : string * hol_type -> unit

Sets up a new binder in the current theory.

A call new_binder(bnd,ty) declares a new binder bnd in the current theory. The type must be of the form ('a -> 'b) -> 'c, because being a binder, bnd will apply to an abstraction; for example

   !x:bool. (x=T) \/ (x=F)

is actually a prettyprinting of

   $! (\x. (x=T) \/ (x=F))

Failure

Fails if the type does not correspond to the above pattern.

Example

   - new_theory "anorak";
   > val it = () : unit

   - new_binder ("!!", (bool-->bool)-->bool);
   > val it = () : unit

   - Term `!!x. T`;
   > val it = `!! x. T` : term

See also

Theory.constants, Theory.new_constant, boolSyntax.new_infix, Definition.new_definition, boolSyntax.new_infixl_definition, boolSyntax.new_infixr_definition, boolSyntax.new_binder_definition