We walk through entry of a display form for the term 
.
Start by creating a new display form object and viewing it. Enter in the ML top loop:
where +scratch is some suitable position in your library. The window initially looks like:
Click MOUSE-LEFT on the first =, to get a text cursor in the empty format sequence on the left-hand side of the definition. Enter the initial text and a slot for the variable:
The definition should now look like:
!<x:var>
== [rhs]
Enter the type slot and the second term slot:
The definition should now look like:
!<x:var>:<T:type:*>. <P:prop
:E>== [rhs]
Now enter the right-hand side of the display form.
Click
MOUSE-LEFT
on the [rhs] placeholder, and
enter exists_unique(T.x.P) as an exploded term.
See Section 
for details on how to do this. Do not fill
in the variable slot or either of the subterm slots. The definition should
now look like:
!<x:var>:<T:type:*>. <P:prop:E>==
Click MOUSE-LEFT on the left-most term slot and to enter the meta terms and meta variable, key:
The definition is now complete. It should look like:
!<x:var>:<T:type:*>. <P:prop:E>==
exists_unique
(<T>;<x>.<P >) This definition includes no linebreaking or parenthesization information. The display form has an open right-hand side, in that there is nothing delimiting the end of the prop slot. We therefore want the layout algorithm to automatically parenthesize the display form. To add parenthesizing attributes, click MOUSE-LEFT on the second = character, to get a term cursor over the whole definition, and then enter:
to get two empty attribute slots, with a term cursor over the first:
::[attr]::
!<x:var>:<T:type:*>.
<P:prop
:E>==
exists_unique
(<T>;<x>.<P>)
To instantiate the attribute slots enter:
To get:
Parens::Prec(exists
)::
!<x:var>:<T:type:*>.
<P:prop:E>== exists_unique
(<T>;<x>.<P>)
Here, we assign the term the same precedence to 
as is assigned in the standard libraries to the 
term.
We illustrate adding extra formats, by adding a soft-break format
such that the 
.
separating the type slot from the prop
slot is only included if the break is not taken.
Click
MOUSE-LEFT
on the 
.
character and delete it using 
C-D
.
Enter:
click
MOUSE-LEFT
on the
after the ? character in the
soft break display form, and enter 
.
.