lean2/tests/lean/implicit1.lean.expected.out

  Set: pp::colors
  Set: pp::unicode
  Assumed: f
∀ a : ℤ, (f a a) > 0
∀ a b : ℤ, (f a b) > 0
  Assumed: g
∀ (a : ℤ) (b : ℝ), (g a b) > 0
∀ a b : ℤ, (g a (f a b)) > 0
  Set: lean::pp::coercion
∀ a b : ℤ, (g a (int_to_real (f a b))) > (nat_to_int 0)
λ a : ℕ, a + 1
Error (line: 10, pos: 18) ambiguous overloads
Candidates:
    Real::add : ℝ → ℝ → ℝ
    Int::add : ℤ → ℤ → ℤ
    Nat::add : ℕ → ℕ → ℕ
Arguments:
    a : ?M0
    b : ?M2[lower:2:2 lift:0:1 subst:0 a]
λ a b c : ℤ, a + c + b
Error (line: 17, pos: 19) ambiguous overloads
Candidates:
    Real::add : ℝ → ℝ → ℝ
    Int::add : ℤ → ℤ → ℤ
    Nat::add : ℕ → ℕ → ℕ
Arguments:
    a : ?M0
    b : ?M2[lower:2:2 lift:0:1 subst:0 a]
  Assumed: x
λ a b : ℤ, a + x + b
-												Modify the parser for accepting expressions such as: 'fun a b, f a b', 'forall a, f a > 0', etc. This is just syntax sugar for 'fun (a : _) (b : _), f a b' and 'forall a : _, f a > 0'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-09-04 00:24:05 +00:00
+								  Set: pp::colors
 								  Set: pp::unicode
 								  Assumed: f
-												Add unicode name for the types: Nat, Int and Real

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-09-04 16:03:41 +00:00
+								∀ a : ℤ, (f a a) > 0
 								∀ a b : ℤ, (f a b) > 0
-												Modify the parser for accepting expressions such as: 'fun a b, f a b', 'forall a, f a > 0', etc. This is just syntax sugar for 'fun (a : _) (b : _), f a b' and 'forall a : _, f a > 0'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-09-04 00:24:05 +00:00
+								  Assumed: g
-												Add unicode name for the types: Nat, Int and Real

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-09-04 16:03:41 +00:00
+								∀ (a : ℤ) (b : ℝ), (g a b) > 0
 								∀ a b : ℤ, (g a (f a b)) > 0
-												Modify the parser for accepting expressions such as: 'fun a b, f a b', 'forall a, f a > 0', etc. This is just syntax sugar for 'fun (a : _) (b : _), f a b' and 'forall a : _, f a > 0'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-09-04 00:24:05 +00:00
+								  Set: lean::pp::coercion
-												Add unicode name for the types: Nat, Int and Real

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-09-04 16:03:41 +00:00
+								∀ a b : ℤ, (g a (int_to_real (f a b))) > (nat_to_int 0)
 								λ a : ℕ, a + 1
-												Modify the parser for accepting expressions such as: 'fun a b, f a b', 'forall a, f a > 0', etc. This is just syntax sugar for 'fun (a : _) (b : _), f a b' and 'forall a : _, f a > 0'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-09-04 00:24:05 +00:00
+								Error (line: 10, pos: 18) ambiguous overloads
 								Candidates:
-												Add unicode name for the types: Nat, Int and Real

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-09-04 16:03:41 +00:00
+								    Real::add : ℝ → ℝ → ℝ
 								    Int::add : ℤ → ℤ → ℤ
 								    Nat::add : ℕ → ℕ → ℕ
-												Modify the parser for accepting expressions such as: 'fun a b, f a b', 'forall a, f a > 0', etc. This is just syntax sugar for 'fun (a : _) (b : _), f a b' and 'forall a : _, f a > 0'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-09-04 00:24:05 +00:00
+								Arguments:
-												Move metavariables to the kernel. This is the first step for implementing the new elaborator.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-09-13 01:25:38 +00:00
+								    a : ?M0
 								    b : ?M2[lower:2:2 lift:0:1 subst:0 a]
-												Add unicode name for the types: Nat, Int and Real

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-09-04 16:03:41 +00:00
+								λ a b c : ℤ, a + c + b
-												Modify the parser for accepting expressions such as: 'fun a b, f a b', 'forall a, f a > 0', etc. This is just syntax sugar for 'fun (a : _) (b : _), f a b' and 'forall a : _, f a > 0'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-09-04 00:24:05 +00:00
+								Error (line: 17, pos: 19) ambiguous overloads
 								Candidates:
-												Add unicode name for the types: Nat, Int and Real

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-09-04 16:03:41 +00:00
+								    Real::add : ℝ → ℝ → ℝ
 								    Int::add : ℤ → ℤ → ℤ
 								    Nat::add : ℕ → ℕ → ℕ
-												Modify the parser for accepting expressions such as: 'fun a b, f a b', 'forall a, f a > 0', etc. This is just syntax sugar for 'fun (a : _) (b : _), f a b' and 'forall a : _, f a > 0'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-09-04 00:24:05 +00:00
+								Arguments:
-												Move metavariables to the kernel. This is the first step for implementing the new elaborator.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-09-13 01:25:38 +00:00
+								    a : ?M0
 								    b : ?M2[lower:2:2 lift:0:1 subst:0 a]
-												Modify the parser for accepting expressions such as: 'fun a b, f a b', 'forall a, f a > 0', etc. This is just syntax sugar for 'fun (a : _) (b : _), f a b' and 'forall a : _, f a > 0'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-09-04 00:24:05 +00:00
+								  Assumed: x
-												Add unicode name for the types: Nat, Int and Real

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-09-04 16:03:41 +00:00
+								λ a b : ℤ, a + x + b