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

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?

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.