Zulip Chat Archive

Stream: new members

Topic: What does ` . obviously` mean?


view this post on Zulip 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?

view this post on Zulip Greg Price (Apr 04 2021 at 08:31):

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

view this post on Zulip Greg Price (Apr 04 2021 at 08:32):

Rather, the definition of obviously is

view this post on Zulip 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

view this post on Zulip Justus Springer (Apr 04 2021 at 08:34):

Thank you!

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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