30 lines
810 B
Text
30 lines
810 B
Text
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
|