mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-16 15:52:43 +03:00
32 lines
376 B
Plaintext
32 lines
376 B
Plaintext
Main> "Int"
|
|
Main> 12
|
|
Main> 12
|
|
Main> 12
|
|
Main> 12
|
|
Main> "Negative Int"
|
|
Main> -12
|
|
Main> -13
|
|
Main> -13
|
|
Main> -13
|
|
Main> "Integer"
|
|
Main> 12
|
|
Main> 12
|
|
Main> 12
|
|
Main> 12
|
|
Main> "Negative Integer"
|
|
Main> -12
|
|
Main> -13
|
|
Main> -13
|
|
Main> -13
|
|
Main> "Double"
|
|
Main> 12.0
|
|
Main> 12.3
|
|
Main> 12.5
|
|
Main> 12.7
|
|
Main> "Negative Double"
|
|
Main> -12.0
|
|
Main> -12.3
|
|
Main> -12.5
|
|
Main> -12.7
|
|
Main> Bye for now!
|