(Created page with " Also have a look at Tips:_Writing_Models_for_ProB. == LET == Classical B only has a LET substitution, no let construct for predicates or expressions. Event-B has no let...") |
|||
| Line 9: | Line 9: | ||
=== Let for predicates === | === Let for predicates === | ||
For predicates this encodes a let predicate: | |||
#x.(x=E & P) | #x.(x=E & P) | ||
corresponds to something like | corresponds to something like | ||
let x=E in P | let x=E in P | ||
Within set comprehensions one can use the following construct: | |||
dom({x,y|y=E & P}) | dom({x,y|y=E & P}) | ||
corresponds to something like | corresponds to something like | ||
Also have a look at Tips:_Writing_Models_for_ProB.
Classical B only has a LET substitution, no let construct for predicates or expressions. Event-B has no let construct whatsoever.
For predicates this encodes a let predicate:
#x.(x=E & P)
corresponds to something like
let x=E in P
Within set comprehensions one can use the following construct:
dom({x,y|y=E & P})
corresponds to something like
{x|let y=E in P}
#UNION(x).(x=E|F)
corresponds to something like
let x=E in F