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?