mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
11 lines
229 B
Plaintext
11 lines
229 B
Plaintext
module IfThenElse
|
|
use mach.java.lang.Integer
|
|
|
|
let test_ite (b0 : bool) (b1 : bool) : integer =
|
|
let x = if b0 then
|
|
if b1 then 2 else 0
|
|
else
|
|
if b1 then 3 else 1 in
|
|
2 * x
|
|
|
|
end |