override_interface : string * term -> unit
Map identifier to specific underlying constant.
A call to override_interface("name",`cname`) makes the parser map
instances of identifier name to whatever constant is called cname. Note
that the term `cname` in the call may either be that constant or a variable
of the appropriate type. This contrasts with overload_interface, which can
make the same identifier map to several underlying constants, depending on
type. A call to override_interface removes all other overloadings of the
identifier, if any.
- FAILURE CONDITIONS
Fails unless the term is a constant or variable.
You might want to make the exponentiation operation EXP on natural numbers
parse and print as `^'. You can do this with
Note that the special parse status (infix in this case) is based on the
interface identifier, not the underlying constant, so that does not make `^'
parse as infix:
val it : unit = ()
but you can do that with a separate parse_as_infix call. It is also
possible to override polymorphic constants, and all instances will be handled.
For example, HOL Light's built-in list operations don't look much like OCaml:
val it : thm = |- (!m. ^ m 0 = 1) /\ (!m n. ^ m (SUC n) = m * ^ m n)
but after a few interface modifications:
val it : thm =
|- (!l. APPEND  l = l) /\
(!h t l. APPEND (CONS h t) l = CONS h (APPEND t l))
it looks closer (you can remove the spaces round :: using
val it : thm = |- (!l.  @ l = l) /\ (!h t l. h :: t @ l = h :: (t @ l))
- SEE ALSO
overload_interface, parse_as_infix, reduce_interface, remove_interface,
the_implicit_types, the_interface, the_overload_skeletons.