|
|
|---|
|
|
|
|---|
Representation of C conditional expressions for ATC.
C conditional expressions and statements are both non-strict, so they both have to be represented by if in ACL2. To provide control on which ifs represent conditional statements and which ifs represent conditional expressions, we provide a function condexpr that is just identity but can be used to wrap an if to signify that it represents a C conditional expression instead of statement. Without that wrapper, an if represents a conditional statement, which is more common than a conditional expression in C.