IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
There is a standard method for flexible entry and editing of dependent type operators in Constable's standard notation.
We'll use dependent function in this explanation.
Constable's notation for dependent function space is
x:AB(x),
with the special case of type independence notated
AB.
The command for inserting this operator is `>'.
Normally, insertion inserts <Type><Type> in left-mode, and [var]:<Type><Type> in right-mode, and replace-mode insertion inserts <Type><Type>.
But if the point is at an instance of ([var]:<type> ?), which is inserted by `:', left-mode insertion will build the dependent form using the typing indicated.
Furthermore, insertion with `:' is specialized in anticipation of this.
Examples:
x:A<Type> can be created by entering
`x' `:' `A' `>' in a plain slot, or
`A' `>' or `>' `A' into the slot of x:<type> ?,
To get at the binding var position which is hidden in
AB, `(c-s)' will temporarily reveal the binding position, and will delete it if it is null.
It is easy to null-out the binding var position in a slot simply by using `(c-u){(tab)(return)}', which will then skip to the next slot if any.
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
B(x)
(return)}'
