Lean: what does the syntax `variable [ring R]` mean?

Question

I have written a simple Lean program, inspired by things I found here and there, which compiles as shown in the web editor:

import algebra.ring.basic 

variable R : Type
variable [ring R]

theorem first_theorem(a : R): -(-a) = a :=
calc
  -(-a) = -(-a) + 0             : by rw add_zero
  ...   = 0 + -(-a)             : by rw add_comm
  ...   = (a - a) + (-(-a))     : by rw sub_self
  ...   = (a + (-a)) + (-(-a))  : by rw sub_eq_add_neg
  ...   = a + ((-a) + -(-a))    : by rw add_assoc
  ...   = a + (-a - (-a))       : by rw sub_eq_add_neg
  ...   = a + 0                 : by rw sub_self
  ...   = a                     : by rw add_zero 

(Sub-question: is there a way to make the web editor show something in the right panel when the theorem is correctly proven? It bothers me that it stays blank...)

My question is basic but I couldn't find an answer in the doc: what does the syntax variable [ring R] mean? I understand that it somehow declares R to be a ring, but why the brackets?

Answer 1

The square brackets means that Ring R is an implicit argument, meaning the Lean will find it by itself when needed. This why you didn't need to give it a name nor to explicitly mention it in your proof. You can learn more about this in the TPIL.