11.7 Value expressions11.7 Value expressions
11 PVS translator 11 PVS translator
11.9 Names 11.9 Names
11.8 Bindings and typings

11.8 Bindings and typings

Bindings and typings are accepted.

RSL allows nested product bindings, but PVS does not. The translation introduces new identifiers of the form prodn_ for inner products, plus let expressions to define the original identifiers in their scopes. For example:

                                     
 let (w,(x,(y,z))) = e in e1 end

translates to 

LET (w,prod1_) = e IN LET (x,prod2_) = prod1_, (y,z) = prod2_ IN e1
Chris George, April 17, 2008

11.8 Bindings and typings
11.7 Value expressions11.7 Value expressions
11 PVS translator 11 PVS translator
11.9 Names 11.9 Names