lean2/tests/lean/793a.lean.expected.out

4 : ℚ
23 / 10 : ℚ
1 : ℚ
10213 / 1000 : ℚ
-(3 / 10) : ℚ
10213 / 1000 : ℚ
23 / 10 : ℚ
1 : ℚ
quot.mk (prerat.mk (int.of_nat 1) (int.of_nat 1) (int.of_nat_succ_pos 0))
-												fix(tests/lean): adjust remaining tests to changes in the standard library

											
										
										
											2015-10-14 01:35:16 +00:00
+: ℚ
 / 10 : ℚ
 : ℚ
 / 1000 : ℚ
-												fix(frontends/lean/parser): add support for decimals

Decimal numbers are notation for rationals.
If rat.of_num is not available, then an error is generated.

closes #793

											
										
										
											2015-08-12 01:43:42 +00:00
+								-(3 / 10) : ℚ
 / 1000 : ℚ
 / 10 : ℚ
 : ℚ
-												fix(tests/lean): adjust remaining tests to changes in the standard library

											
										
										
											2015-10-14 01:35:16 +00:00
+								quot.mk (prerat.mk (int.of_nat 1) (int.of_nat 1) (int.of_nat_succ_pos 0))