syntax / structure of (most common) proofs?

Stream: new members

[rzeta0]

So as a beginner I naturally struggle to understand some of the syntax I'm seeing around the web.

I have tried to find answers but can't find a simple guide that just explains what the syntax of (the most common) proofs.

I am guess it is something like the following - but I can't find an easy to read guide that confirms it:

name can be anything {variable type declarations} (hyopthesis) (hyopthesis) : statement to prove :=
 method eg calc
 statement 1 = statement 2 := by  tactic
 statement 2= statement 3 := by tactic
 ...
 _ = conclusion statement to prove := by tactic

Is this correct?

I've seen "example" used for the name a lot, which makes me thing the name isn't arbitrary.

[Ralf Stephan]

That is one of many formats, a calc proof, see doc#calc.html. To get a better overview I'd suggest #tpil.

[Kyle Miller]

which makes me thing the name isn't arbitrary

If you use the example ... command then the theorem is checked and thrown away. If you use theorem foo ... then the theorem is checked and you can refer to it in future proofs as foo.

[rzeta0]

Thanks both - looks like I now need to learn about "modes" as that page refers to them - tactic mode, term mode,...

[Kevin Buzzard]

by switches Lean from term mode to tactic mode, and exact switches it from tactic mode to term mode.

[Ralf Stephan]

Isn't term mode the pure functional language vs. tactics being a language inside that language?