Zulip Chat Archive

Stream: general

Topic: tip for filling in holes


view this post on Zulip Kevin Buzzard (Apr 20 2018 at 10:11):

Sometimes in Lean you sit down to write a definition or a theorem, knowing that it will be really easy and fun. I was just in that situation. I need to write down some maps between localized rings and prove that they have some properties, but now I know that the localization interface is excellent and that pretty much every single one of my proofs will look like name_of_function _ _ _ _ _.

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 10:12):

However, I have run into an unexpected annoyance.

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 10:12):

Here is my skeleton set-up.

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 10:12):

definition localization.loc_loc_is_loc {R : Type u} [comm_ring R] {f g : R} (H : Spec.D' g  Spec.D' f) :
(localization.away g) ≃ᵣ localization.away (localization.of_comm_ring R (powers f) g) :=
{ to_fun := _,
  inv_fun := _,
  left_inv := _,
  right_inv := _,
  is_ring_hom := _
}

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 10:12):

The idea now is that I just fill in all the holes one by one.

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 10:13):

But I want the holes to have red squiggles under them!

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 10:13):

And for some reason, only the last one does

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 10:14):

and the associated complaint is full of metavariables

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 10:14):

because it depends on some earlier holes

view this post on Zulip Kenny Lau (Apr 20 2018 at 10:14):

begin end

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 10:14):

and then remove it later?

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 10:14):

because it's a def

view this post on Zulip Kenny Lau (Apr 20 2018 at 10:14):

i just fill in stuff in front of begin end

view this post on Zulip Kenny Lau (Apr 20 2018 at 10:14):

I mean, replace your _ with begin end

view this post on Zulip Kenny Lau (Apr 20 2018 at 10:15):

I can show you that in person next week ^^

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 10:15):

begin exact _ end

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 10:15):

:-)

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 10:15):

Many thanks Kenny!

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 10:16):

I feel like there are so many little tips like this, and it's unclear to me where they should be put.

view this post on Zulip Kenny Lau (Apr 20 2018 at 10:16):

you don’t need exact _


Last updated: May 08 2021 at 19:11 UTC