## Stream: general

### Topic: crazy construction of a structure

#### 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).

#### Kevin Buzzard (May 19 2018 at 19:40):

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

#### 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⟩


#### 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"

#### Kevin Buzzard (May 19 2018 at 19:42):

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

#### 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

#### 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.

#### Patrick Massot (May 19 2018 at 19:45):

This pattern has been discussed many times here

#### Patrick Massot (May 19 2018 at 19:45):

Put every definition in the refine and then proofs

#### Patrick Massot (May 19 2018 at 19:46):

The .. at the end is important

#### 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

#### 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

#### 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 ..

#### Patrick Massot (May 19 2018 at 20:40):

I think

Last updated: May 14 2021 at 06:16 UTC