3
$\begingroup$

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?

$\endgroup$

1 Answer 1

3
$\begingroup$

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.

$\endgroup$
2
  • 1
    $\begingroup$ instance implicit, no? $\endgroup$ Sep 20, 2023 at 16:42
  • $\begingroup$ Yes, it is an instance, so it is found by typeclass search, not by unification. $\endgroup$
    – Ricky
    Sep 21, 2023 at 8:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.