.. _dot_notation:

Dot notation
============

Say you have a type, like ``subgroup G``, and a term of that type, like ``H : subgroup G``. Say you have a function in the ``subgroup`` namespace which takes as input a term of type ``subgroup G``, for example ``subgroup.inv_mem``, which has as an explicit input a term ``H : subgroup G`` and spits out a proof that ``x ∈ H → x⁻¹ ∈ H``. Then instead of writing ``subgroup.inv_mem H : x ∈ H → x⁻¹ ∈ H`` you can just write ``H.inv_mem : x ∈ H → x⁻¹ ∈ H``.

In general the rule is that if you have a term ``H : foo ...`` of type ``foo`` or ``foo A B`` or whatever, and then you have a function called ``foo.bar`` which has an explicit (i.e., round brackets) input of type ``foo ...``, then instead of ``foo.bar H`` you can just write ``H.bar``. This is why it's a good idea to define theorems about ``foo``s in the ``foo`` namespace.

This sort of trick can be used all over the place; it's surprisingly powerful. For example Lean has a proof ``eq.symm : x = y → y = x``. If you have a term ``h : a = b`` then, remembering that ``=`` is just notation for ``eq`` so that ``h`` really has type ``eq a b``, you can write ``h.symm : b = a`` as shorthand for ``eq.symm h``.