| #check 1.2 | |
| #check 1.2 + 2.3 | |
| #check 1.0 | |
| #eval 1.2 + 2.3 | |
| #check 1. | |
| #check 3.1416 | |
| theorem ex : 31416e-4 = 3.1416 := | |
| rfl | |
| #eval 3.4e-100 * 1e98 | |
| #eval 12.3e90 * 1E-90 | |
| #eval 3.00e-100 * 1e100 | |
| #eval 3.00e-100 * 1.e100 | |
| #eval 3.00e-100 * 1.0e100 | |
| #eval 1e10 | |
| #eval 1e50 | |
| #eval 1e80 | |
| #eval 1e100 | |
| #eval 1e200 | |
| #eval 1e300 | |
| #eval 1e400 | |
| #eval 1 / 1e-1 | |
| #eval 1 / 1e-2 | |
| #eval 1 / 1e-10 | |
| #eval 1 / 1e-100 | |
| #eval 1 / 1e-200 | |
| #eval 1 / 1e-400 |