.Open CONVENIENCES

. Summary
.Table
Name    Sample
.Row
Substitutions
.Item
( x^2+x/(1+x) where x=(exp(y+sin(z)) )  
.Row
Partial Descriptions
.Item
data::=good_data|...
.Row Enumerated types
.Item direction::={east, west, north, south}.
.Row Inequality
.Item Two notations: x!=y(C), x<>y (Pascal)
.Close.Table

.Open Substitutions
Substitutions create local  or private dfinitions that have no meaning outside of the formula or documentation that they are defined.
. Example of Substitution
        (a*x^2+b*x+c where x=3) = for x:=3( a*x^2+b*x+c ) = (9a + 3b +c).

Both forms bind values to abbreviations in a small area of text only.  
. Syntax of Substitution
substitution::="(" expression "where" tight_binding #{","tight_binding} ")" | "for" tight_binding #(","tight_binding) "(" expression ")"


. Semantics of Substitution
Both forms bind values to abreviations for the range of a single expression.
Notice that in a tight binding it is not permitted to use the variable as part of the expression that represents its value.   This implies that the variable can be replaced by the original without change of meaning.
A formula like
        (a*x^2+b*x+c where x=3)
or      for x=3( a*x^2+b*x+c )

becomes
        (9a + 3b +c)

.Close Substitutions
.Open Partial Descriptions, Ellipsis, and Enthymemes
When writing documentation it is usually easier to develop definitions piece meal rather than with all options, constraints, and complications at the same time.  The tool for keeping this under control is the Ellipsis symbol ("..."). For example one technique is to start with a broad concept and then add more and more constraints.  Thus if a term, `t` is  defined as
	t::= A & B & C

then we can quote as facts.
	|- t::=A &...
	|- t::=B &...

It is convenient to allow these to be valid input into a documentation system:  
	restriction::=described_term "::=" intersection "&...", 

A described term is always the name of a set of possibilities and so can have many descriptions. It must satisfy them all.  If `t::=S&...` then `t` represents  the largest subset `S` that is a subset of all other descriptions.  A term with a definition can be quoted as a description. If declared, then a term that is described as a set of type `S` must be declared as type `@S`. Chapter 5 provides the semantics of definitions in general. 

It is best to start from a specific, easily understood subset of the problem and progress to more general forms[Botting 84b].   The development of error handling is an ubiquitous example:  
	all_possible_data::=good_data | erroneous_data | other_data

So is that of a compiler:  
	compile::=compile_good_program | check_bad_program | reject_non_program

Thus given that
	t::=A | B | C, 

then we can quote the following
	|- t::=A |..., 
	|- t::=B |... .

Again it should be possible to input a series of additional alternatives into a documentation processor, and have them, checked, appended, etc.
	additional_alternative::=described_term "::=" selection "|..." 

Formally a set of additional alternatives are combined into a single definition where the term is defined as the union of the separate alternatives.

It is incorrect to use more than one ellipsis on the same term. 
	description::=additional_alternative | restriction

These notations are conveniences. Formally they do not exist. They become a set of definitions that are created by either the intersection or union of all the descriptions.

An incomplete argument is called an `enthymeme`[Aristotle?].  In MATHS it 
is an argument with any contiguous set of steps replace by the ellipsis 
(...) symbol (see Chapter 5).  Similarly the ellipsis can be used  inside 
any set of documentation to hide a piece of irrelevant documentation from 
the reader/user.  Online the three dots could react to being selected by 
expanding to show the details.

A third form of incompleteness occurs when part of a sequence is left out.  Similar - but much more informal  - is the use of the ellipsis  "..." in  mathematical expressions :  
	n*(n+1)/2 = 1+2+3+...+n

as in the design of bin.p above.  These can only be verified if they are accompanied with a formal expression that makes clear what is meantSubstitutions

Finally, if the class of a structured object is given (C) and a tight enough condition(P) specified,  then missing attributes can be predicted that make the object fit the class.  Formally, suppose that C is a class with structure N and P a boolean expression containing variable of N then:
	the C(P) ::= the{ $(N) : C || P} = the $ $N and $(N) in C and P.

Similarly if C has identifers k and data d (C : @N(k)->(d)) then
	the C(k1=>a1, k2=>a2, ...) ::= the C(k1=a1 and k2=a2 and ...).

The following syntax is a natural alternative:
	"the" Base "with" Bindings

	(the B with L) ::= the{ x:set B || L }
.Close Partial Descriptions, Ellipsis, and Enthymemes

.Open Enumerated types
A definition like
.As_is 		direction::={east,north, west, south).
implies
.As_is 		direction::Sets.
.As_is 		east::direction.
.As_is 		north::direction.
.As_is 		west::direction.
.As_is 		south::direction.
.As_is 		|- direction = {east,north, west, south).
In general a defition of a new type as a set of new variables,
implicitly declares the variables.

.Close Enumerated types
. Inequality
The operator "=" indicates identity or equality.  There are two traditional symbols
for inequality: "!=" and "<>".  Both are (now) leagle in MATHS.
.Close CONVENIENCES