unparse_as_binder : string -> unit

SYNOPSIS

Stops the quotation parser from treating a name as a binder.

DESCRIPTION

Certain identifiers c have binder status, meaning that `c x. y` is parsed as a shorthand for `(c) (\x. y)'. The call unparse_as_binder "c" will remove c from the list of binders if it is there.

FAILURE CONDITIONS

Never fails, even if the string was not a binder.

EXAMPLE

  # `!x. x < 2`;;
  val it : term = `!x. x < 2`

  # unparse_as_binder "!";;
  val it : unit = ()
  # `!x. x < 2`;;
  Exception: Failure "Unexpected junk after term".

COMMENTS

Removing binder status for the pre-existing binders like the quantifiers should only be done with great care, since it can cause other parser invocations to break.