design choice about cursor focus

[ivoysey]

p. 6 Rule (10a) Why does the construct arrow make the type at the cursor
location into the argument type?  Why not the result type?  Why not have
two commands for introducing function types, one where the cursor into the
argument and a second into the return?  This approach would be consistent
with what you did for function application.

p. 7 Similarly for plus.  Why does the construct plus command put the
argument in the left hand side?  Because of the symmetry of addition?

[ivoysey]

we promised

Good points! The decision to leave the expression under the cursor on the
left is formally an arbitrary one. We made the choice based on our
intuition that programs are typically written “left to right”, i.e. in a
textual language one typically writes the left side of an arrow type or
addition before writing down “->” or “+” and then the right side. It would
be possible to include a variant of these actions that made the opposite
decision, by analogy to the construct arg action. Alternatively, some or
all of these could be derived actions as described above. We will take care
to indicate which aspects of our calculus are based on informal intuitions
like this in the final version.