--- layout: archive title: Zulip Chat Archive permalink: /stream/113488-general/topic/crazy.20construction.20of.20a.20structure.html ---
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).
Here are the two ways I knew of building instances of a structure:
structure foo := (bar : ℕ) (baz : Prop) definition x : foo := { bar := 34, baz := 2 + 2 = 5 } definition y : foo := ⟨3,true⟩
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
"
The first one I always just assumed was custom notation that only made sense for structures
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
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.
This pattern has been discussed many times here
Put every definition in the refine and then proofs
The ..
at the end is important
Well, really the tactic is refine ...; { ... }
and these other {}
s are solve_one begin ... end
or whatever
The
..
at the end is important
I don't see any ..
at the end in my link
That's because there are underscores around. If you do what I wrote (define operations, leave out proofs), you need ..
I think
{% endraw %}Last updated: Apr 24 2020 at 19:02 UTC