Shortcut for introducing fresh constant

[phlegmaticprogrammer]

I had a discussion with Phil about how I dislike the current way of dealing with introducing new constants in library code which cannot assume any assumptions about the context into which the new constant is introduced:

val x = fresh "x"
let '‹x›'
...

Phil suggested that instead of the above, the following should be enough:

let '‹x›'

The interpreter / compiler checks if x is an uninitialised variable. If so, it automatically generates a val x = fresh "x" automatically!

This strategy should work for let introduction, let definition, and for choose.

[phlegmaticprogrammer]

I think the following solution is easier to detect for the casual code reader, and should also be more easily implementable for the interpreter.

let '‹val x›'

would be short for

val x = fresh "x"
let '‹x›'
x = '‹x›'

[phlegmaticprogrammer]

As an addition, to fit this into the linear scope thing, there is also a possibility to use the shortcut via assign (=), not via val:

let '‹= x›' 

assumes that x is already in linear scope.