Zulip Chat Archive

Stream: new members

Topic: No has_lt typeclass instance for rational number


view this post on Zulip 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 [1], 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:

  1. why there is not has_lt typeclass for rationals (is there something I am missing obvious)?
  2. when I am import data.real.basic, is ℚ is coerced to ℝ?

[1] https://leanprover-community.github.io/mathlib_docs/data/rat/basic.html

view this post on Zulip Johan Commelin (Jul 12 2020 at 04:22):

@Mukesh Tiwari https://leanprover-community.github.io/mathlib_docs/data/rat/order.html

view this post on Zulip Mukesh Tiwari (Jul 12 2020 at 04:28):

@Johan Commelin Thank you very much.

view this post on Zulip Jalex Stark (Jul 12 2020 at 10:35):

Imports are transitive

view this post on Zulip Jalex Stark (Jul 12 2020 at 10:36):

So you import the file that Johan pointed to when you say import data.real.basic


Last updated: May 13 2021 at 17:42 UTC