search

jrh13 / hol-light

The HOL Light theorem prover
Other
435 stars 78 forks source link

Enable more descriptive names for quantifiers and logical constants #111

Closed jargh closed 2 months ago

jargh commented 2 months ago

The new functions "set_verbose_symbols" and "unset_verbose_symbols" enable and disable, respectively, more verbose and descriptive names for some logical symbols; these are now enabled by default:

    F -> false
    T -> true
    ! -> forall
    ? -> exists
    ?! -> existsunique

This is all done via interface maps. Not only is the underlying term structure unchanged (the "actual" names are the symbolic ones) but also the original syntax is accepted as an alternative:

exists x. x = 1 = ?x. x = 1;;

val it : bool = true