Zulip Chat Archive

Stream: new members

Topic: brakets, keys and parenthesis


Esteban Estupinan (Jun 13 2021 at 18:14):

hi i m seeing theorems, structures, definitions in mathlib web page. All those has something in similar, after the name of definition, theorem or structure and before the colon, there are expressions between brakets, keys or parenthesis. Please in very homemade words what is the difference write expressions in brakets, keys and parenthesis what do they symbolize in the proof. for example

Esteban Estupinan (Jun 13 2021 at 18:14):

imagen.png

Kevin Buzzard (Jun 13 2021 at 18:42):

#tpil

Kevin Buzzard (Jun 13 2021 at 18:42):

It's all explained in that book

Esteban Estupinan (Jun 13 2021 at 18:57):

specifically in what chapter?

Kevin Buzzard (Jun 13 2021 at 18:58):

Read the first three chapters and this will get you started. Then ask again if there are still things you don't understand.

Alex J. Best (Jun 13 2021 at 18:59):

The {} are https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#implicit-arguments. And the [] are https://leanprover.github.io/theorem_proving_in_lean/type_classes.html. But to understand those completely there are other things in between that you'd need to read too

Esteban Estupinan (Jun 13 2021 at 21:27):

ok curly brackets is an implicit argument

Esteban Estupinan (Jun 13 2021 at 22:00):

i m reading "mathematics_in_lean" book, here effectively explain about curly brackets and parenthesis, but in pg 10 and 27 squere brackets is mentioned. In the book is written pages forward the use of square brackets, but i dont find, someone help what part of this books explains square brackets use? mathematics_in_lean.pdf

Kevin Buzzard (Jun 13 2021 at 22:13):

We haven't got to type classes yet. You're better off reading the TPIL link above

Esteban Estupinan (Jun 13 2021 at 22:34):

oh I understand better math.. book . I hope that some time complement this part of square brackets


Last updated: Dec 20 2023 at 11:08 UTC