FDL > PVS > Prelude > booleans : Theory

PVS-2.4 prelude.pvs

 booleans declares the type boolean and its abbreviation bool, along
 with the boolean constants true and false and the boolean connectives.
 The properties of the connectives are given later, but the connectives
 are built in to the typechecker so must be provided early on.
 Note: the boolean type could be defined as the enumeration type {false,
 true}, but booleans are primitive; the correct handling of enumeration
 types requires the boolean type.

booleans : THEORY
BEGIN

boolean : NONEMPTY_TYPE

bool : NONEMPTY_TYPE = boolean

FALSE: bool ;

TRUE: bool ;

NOT: [bool- > bool] ;

AND: [bool, bool- > bool] ;

& : [bool, bool- > bool] ;

OR: [bool, bool- > bool] ;

IMPLIES: [bool, bool- > bool] ;

= > : [bool, bool- > bool] ;

WHEN: [bool, bool- > bool] ;

IFF: [bool, bool- > bool] ;

< = > : [bool, bool- > bool] ;

END booleans