promote hypothesis to fact instance

Stream: new members

[Jalex Stark]

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

[Jalex Stark]

ah, it's this

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