Zulip Chat Archive

Stream: new members

Topic: promote hypothesis to fact instance


view this post on Zulip Jalex Stark (Jun 17 2020 at 20:18):

during a proof, I create a nat p and prove that it's prime. then i want instance search to figure out that zmod p is a field, presumably by first knowing that p is prime. How do I do that?

import data.zmod.basic

example {p : } [fact p.prime] : field (zmod p) :=
begin
  apply_instance,
end

example {p : } (hp : p.prime) : field (zmod p) :=
begin
  have : fact p.prime, exact hp,
  apply_instance,
end

view this post on Zulip Jalex Stark (Jun 17 2020 at 20:19):

ah, it's this

example {p : } (hp : p.prime) : field (zmod p) :=
begin
  haveI : fact p.prime := hp,
  apply_instance,
end

Last updated: May 12 2021 at 05:19 UTC