mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
15 lines
233 B
Plaintext
15 lines
233 B
Plaintext
theory Number
|
|
|
|
use int.Int
|
|
use real.RealInfix
|
|
|
|
goal dec : 123 = 100 + 23
|
|
goal hex : 0x7b = 100 + 23
|
|
goal oct : 0o173 = 100 + 23
|
|
goal bin : 0b1111011 = 100 + 23
|
|
|
|
goal real : 1.23e2 = 100. +. 23.
|
|
goal hexa : 0x7.bp4 = 100. +. 23.
|
|
|
|
end
|