Zulip Chat Archive

Stream: new members

Topic: Using div_self


view this post on Zulip Eric Wieser (Jun 17 2020 at 14:53):

Having some difficulty applying div_self to a trivial goal:

type mismatch at application
  div_self h2
term
  h2
has type
  z - 1  0
but is expected to have type
  ?m_2  0
state:
z : ,
h : ¬z = 1,
h2 : z - 1  0
 (z - 1) / (z - 1) = 1

it looks to me like those types should match?

view this post on Zulip Jalex Stark (Jun 17 2020 at 14:53):

do #check div_self

view this post on Zulip Eric Wieser (Jun 17 2020 at 14:55):

I get div_self : ?M_3 ≠ 0 → ?M_3 / ?M_3 = 1

I don't quite get how it decides to fill the M_3 placeholder. M_3 is implicit, so I was hoping it could be inferred from h2 as z-1.

view this post on Zulip Jalex Stark (Jun 17 2020 at 14:56):

it's going to have a type variable requiring a typeclass that the integers don't satisfy, maybe division_ring or something

view this post on Zulip Eric Wieser (Jun 17 2020 at 14:57):

Is there an equivalent for integers?

view this post on Zulip Reid Barton (Jun 17 2020 at 14:58):

if there is then hopefully it has a name like int.div_self

view this post on Zulip Eric Wieser (Jun 17 2020 at 14:59):

For whatever reason that was not autocompleting...

view this post on Zulip Jalex Stark (Jun 17 2020 at 15:02):

https://leanprover-community.github.io/mathlib_docs/data/int/basic.html#int.div_self

view this post on Zulip Jalex Stark (Jun 17 2020 at 15:02):

do you have import data.int.basic in your file?

view this post on Zulip Kevin Buzzard (Jun 17 2020 at 15:16):

#check @div_self is the thing to do in this situation -- you see immediately what typeclass it wants


Last updated: May 14 2021 at 03:27 UTC