FDL > PVS > Prelude > if_def : Theory

PVS-2.4 prelude.pvs

 if_def provides the polymorphic declaration of the IF-THEN-ELSE
 connective.  Note that the declaration for IF is for a 3-ary function,
 and that the IF-THEN-ELSE form is simply an alternative syntax.

if_def [T:TYPE] : THEORY
BEGIN

%%(TCC) IF_TCC1: OBLIGATION

IF: [boolean, T, T- > T] ;

END if_def