Stream: new members
Mukesh Tiwari (Jul 12 2020 at 03:44):
Below is the code, which makes Lean typechecker unhappy:
import data.nat.basic data.rat.basic def neg_fn (μ : ℕ → ℚ) : Prop := ∀ (c : ℕ), ∃ (n₀ : ℕ), ∀ (n : ℕ), n ≥ n₀ → (μ n) * (n ^ c) < 1
and the error I am getting is:
failed to synthesize type class instance for has_lt ℚ:
μ : ℕ → ℚ, c n₀ n : ℕ, a : n ≥ n₀ ⊢ has_lt ℚ
By looking at the documentation , I see there is no has_lt instance for rationals. However, the error goes away if I import data.real.basic (but not changing anything else). So my questions are:
- why there is not has_lt typeclass for rationals (is there something I am missing obvious)?
- when I am import data.real.basic, is ℚ is coerced to ℝ?
Johan Commelin (Jul 12 2020 at 04:22):
Mukesh Tiwari (Jul 12 2020 at 04:28):
@Johan Commelin Thank you very much.
Jalex Stark (Jul 12 2020 at 10:35):
Imports are transitive
Jalex Stark (Jul 12 2020 at 10:36):
So you import the file that Johan pointed to when you say
Last updated: May 13 2021 at 17:42 UTC