LP, the Larch Prover  Overloaded identifiers
LP allows users to overload identifiers for variables and
operators. For example, LP allows the simple identifier
s to be used both as a function s:Nat>Nat and as a variable
s:Set, and it allows the operator identifier  to be used both as a
prefix operator and as an infix operator. LP automatically overloads the
predefined equality and conditional
operators (=, ~=, and if__then__else__), once for each declared
sort. There are only two restrictions on overloading:

The same identifier cannot be used to name a variable and a constant (i.e., a
nullary operator) of the same sort.

The logical, equality, and conditional operators (except for ~) cannot be
overloaded with userdefined signatures.
LP disambiguates user input by using context to associate each identifier with
a previous declaration. When context permits more than one association, users
must supply additional annotations to resolve the ambiguity.
Disambiguating terms
Users can resolve potential ambiguities in terms by qualifying selected
subterms with their sorts. For example, given the declarations
declare variables x, y, z: Bool, x, y, w: Nat
the terms x = z and x = w are unambiguous, but the term x = y is
ambiguous. It can be disambiguated in several ways, for example, as
x:Nat = y or as x = y:Bool. Given the additional declarations
declare operators f:Nat>Nat, f:Nat>Bool, f:Bool>Bool
the term f(z) is unambiguous, but the term f(w) needs to be
disambiguated as either f(w):Nat or f(w):Bool, and the term f(x)
needs to be disambiguated as one of f(x:Bool), f(x:Nat):Nat, or
f(x:Nat):Bool.
Another potential ambiguity in terms arises from the treatment LP accords to
the period symbol (.). For example, given the declarations
declare operators
1, min: > Nat
a: > Array
__.__: Array, Nat > Nat
__ .size, __ .min: Array > Nat
..
the terms a.size and a.1 are unambiguous, but a.min could
represent an application of either the infix operator . or the postfix
operator .min. In such cases, LP disambiguates a.min as containing a
postfix operator; users who want . to refer to the infix operator can
write a.(min).
Disambiguating operators outside of terms
Users can resolve an ambiguous operator identifier by qualifying it with its
signature or by decorating it with one or two markers (__) to indicate
whether it is an infix, postfix, or prefix operator.
See also