Lifted Domains
The lifting domain builder ( ) ? creates the domain A?a collection of the members of A plus an additional distinguished element ?
The disassembly operation builder converts an operation on A to one on A?for (?x.e):A? B?:
(?x.e):A ? ? B?:is defined as (?x.e) ? = ?
(?x.e)a =[a/x]e for a ? ?
An operation that maps a ? argument to a ? is called strict. Operations that map ? to a proper element are called nonstrict.