Let Expressions

The Idea

• Expressions of the form $let(types,defns,t)
• Replaces the old $let_tt, $let_tf, $let_ft, and $let_ff
• Let expressions removed from plain TFF

Examples

• p: ($int * $int) > $o
  $let(c: $int,c:= $sum(2,3),p(c,c))
• $let(max: ($real * $real) > $real,
       max(X,Y):= $ite($greatereq(X,Y),X,Y),
       max(max(a,b),c) )
• a: $i      b: $i      p: ($i * $i) > $o
  $let([a:$i,b:$i],[a:=b, b:=a],p(a,b))
  $let([a:$i,b:$i],[a,b]:=[b,a],p(a,b))
• i: $int      f: ($int * $int * $int * $int) > $int      p: $int > $o
  $let([ff: ($int * $int) > $int, gg: $int > $int],
       [ff(X,Y):=f(X,X,Y,Y), gg(Z):=f(Z,Z,Z,Z)],
       p(ff(i,gg(i))))