Function definitions inside let blocks

[gisellemnr]

Superficially, there are two cases for functions declared in let blocks, depending on where this let block is:

(* let block in a value declaration *)
val n = let
  fun h x = x + 10
in
  h 7
end

(* let block in a function declaration *)
fun f x = let
  val n = 2
  val m = let 
    fun g 0 x = 0
      | g y x = x + (g (y-1) x)
  in
    g n x
  end
in
  x + m
end

g could be declared using Equations as:

Equations f (x: nat) : nat :=
f x := 
  let n := 2 in
  let m := g n x in
x + m
where g (n: nat) (y : nat) : nat := 
g 0 y := 0 ;
g n y := y + (g (n-1) y)
.

But h cannot be declared using Equations, since this is a top level declaration. Our options are:

• use Equations to declare functions inside let-blocks in function declarations, and use let/fix for those in value declarations;
• move functions such as h outside the let block (this does not sound like a good idea since we are changing the scope)

[gisellemnr]

Tricky example:

fun g x = let
  fun g y = y + 1
  in 
    g x
  end

Also, if the nesting has more than two levels, translating it into Equations using where would flatten the structure.