Zulip Chat Archive

Stream: general

Topic: crazy construction of a structure


view this post on Zulip Kevin Buzzard (May 19 2018 at 19:39):

I never knew one could do this: https://github.com/leanprover/mathlib/blob/38d553694351f4c23a8a8216038c7c8abcb7cd32/ring_theory/localization.lean#L80 (definition of ring structure on a localization).

view this post on Zulip Kevin Buzzard (May 19 2018 at 19:40):

Here are the two ways I knew of building instances of a structure:

view this post on Zulip Kevin Buzzard (May 19 2018 at 19:40):

structure foo :=
(bar : ) (baz : Prop)

definition x : foo := {
  bar := 34,
  baz := 2 + 2 = 5
}

definition y : foo := 3,true

view this post on Zulip Kevin Buzzard (May 19 2018 at 19:41):

The second one I always think of as "pointy brackets are a generic way of building something which needs two (say) "inputs", like a proof of P and Q"

view this post on Zulip Kevin Buzzard (May 19 2018 at 19:42):

The first one I always just assumed was custom notation that only made sense for structures

view this post on Zulip Kevin Buzzard (May 19 2018 at 19:43):

I don't really know what the link is doing, but I do know that by {blah,blah,blah} is pretty much the same as (begin blah,blah,blah, end), which is surely a different usage of the squiggly brackets

view this post on Zulip Reid Barton (May 19 2018 at 19:44):

by takes a tactic. The tactic is refine ....
refine takes an expression with some holes. The expression is { ... }. Here the {...} are building a structure, like you already know.

view this post on Zulip Patrick Massot (May 19 2018 at 19:45):

This pattern has been discussed many times here

view this post on Zulip Patrick Massot (May 19 2018 at 19:45):

Put every definition in the refine and then proofs

view this post on Zulip Patrick Massot (May 19 2018 at 19:46):

The .. at the end is important

view this post on Zulip Reid Barton (May 19 2018 at 19:46):

Well, really the tactic is refine ...; { ... } and these other {}s are solve_one begin ... end or whatever

view this post on Zulip Kevin Buzzard (May 19 2018 at 20:36):

The .. at the end is important

I don't see any .. at the end in my link

view this post on Zulip Patrick Massot (May 19 2018 at 20:39):

That's because there are underscores around. If you do what I wrote (define operations, leave out proofs), you need ..

view this post on Zulip Patrick Massot (May 19 2018 at 20:40):

I think


Last updated: May 14 2021 at 06:16 UTC