Skip to main content

int_max

Function int_max 

Source
fn int_max(n: &str) -> bool
Expand description

Comparison / absolute-value / negation / saturating & unchecked arithmetic operations. Each is modelled with a precise expression over its operands (see the eff_return_* builders) so non-zero-ness is discharged conditionally — only when the operands are actually non-zero.