crazy construction of a structure

Stream: general

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

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

definition y : foo := ⟨3,true⟩

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

This pattern has been discussed many times here

[Patrick Massot]

Put every definition in the refine and then proofs

[Patrick Massot]

The .. at the end is important

[Reid Barton]

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

[Kevin Buzzard]

The .. at the end is important

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

[Patrick Massot]

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

[Patrick Massot]

I think