## Stream: new members

### Topic: What does  . obviously mean?

#### Justus Springer (Apr 04 2021 at 08:29):

I've seen this a lot in the category theory library, e.g.

structure functor (C : Type u₁) [category.{v₁} C] (D : Type u₂) [category.{v₂} D] :
Type (max v₁ v₂ u₁ u₂) :=
(obj []    : C → D)
(map       : Π {X Y : C}, (X ⟶ Y) → ((obj X) ⟶ (obj Y)))
(map_id'   : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X) . obviously)
(map_comp' : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = (map f) ≫ (map g) . obviously)


What does . obviously mean?

#### Greg Price (Apr 04 2021 at 08:31):

It's explained here:
https://leanprover-community.github.io/mathlib_docs/tactic/obviously.html

#### Greg Price (Apr 04 2021 at 08:32):

Rather, the definition of obviously is

#### Greg Price (Apr 04 2021 at 08:32):

The . foo syntax it's being used in is a way of supplying a tactic that gets used to fill in the field by default, if you don't supply one at the time of constructing a structure

Thank you!

#### Justus Springer (Apr 04 2021 at 08:34):

Greg Price said:

It's explained here:
https://leanprover-community.github.io/mathlib_docs/tactic/obviously.html

Somehow I missed that

#### Greg Price (Apr 04 2021 at 08:39):

Ah, to be clear, I didn't mean to suggest that you should have found that already!

#### Greg Price (Apr 04 2021 at 08:39):

The syntax especially is a bit, er, non-obvious until you've seen an explicit discussion of what it means

#### Kevin Buzzard (Apr 04 2021 at 09:03):

The . tactic notation is explained in the lean 3 reference manual here

Last updated: May 14 2021 at 02:15 UTC