Measures for inline function definitions don't work

[nickbattle]

Consider the following:

	f: nat -> nat
	f(x) ==
		let g: nat -> nat
			g(a) ==
				if a = 0 then 0 else a + g(a-1)
			pre a > 0
			measure a
		in
			g(x);

> p f(1)
Error 4034: Name 'measure_g' not in scope in 'DEFAULT' (test.vdm) at line 8:21

The problem is that the FunctionValue created by g does not include a measure function (though it does include a pre_g).

[nickbattle]

The "measure" function within a FunctionValue is looked up on the fly, presumably as a hangover from being able to specify measures as the name of a function rather than as an expression. But the Context create that includes "g" (above) does not include a function for "measure_g" because the creation of the Context does not recurse into FunctionValues to see what they "create". It works for pre/post because their FunctionValues can be computed when the containing FunctionValue is defined.

This suggests the solution is to define "measure_g" in the same way as pre_g/post_g, and only do the name lookup if the measure "name" option is used. But be careful about polymorphic and curried functions, which can be awkward.