Where are double colons used?

Stream: lean4

[Shreyas Srinivas]

A little snippet from #tpil4 shows that when declaring a structure one uses double colons if one wants to explicitly declare its fields as part of a single constructor like mk:

namespace Hidden
structure Prod (α : Type u) (β : Type v) where
  mk :: (fst : α) (snd : β)
end Hidden

Is there any other place where the :: is used for type annotations?

[Kyle Miller]

For what it's worth, you can put this mk :: in a few places that let you use the parenthesis-less notation for explicit fields.

structure Prod (α : Type u) (β : Type v) where mk ::
  fst : α
  snd : β

structure Prod (α : Type u) (β : Type v) where
  mk ::
  fst : α
  snd : β

[Kyle Miller]

This use of :: is unique to structure commands

[Kyle Miller]

In Lean.Parser.Command you can find

def «structure»          := leading_parser
    (structureTk <|> classTk) >> declId >>
    ppIndent (many (ppSpace >> Term.bracketedBinder) >> optional «extends» >> Term.optType) >>
    optional ((symbol " := " <|> " where ") >> optional structCtor >> structFields) >>
    optDeriving

where

def structCtor           := leading_parser
  atomic (ppIndent (declModifiers true >> ident >> " :: "))

[Kyle Miller]

(I didn't know there was a declModifiers in there before the ident. That means that you can for example put protect before mk to protect the constructor.)

[Shreyas Srinivas]

okay, so this is a one-off case. Thanks :). I have never seen :: used in lean anywhere , except when reading #tpil4

[Mario Carneiro]

The more common use is for the "cons" operation on lists

[Shreyas Srinivas]

Ah yes. I should have clarified that I was thinking about type declarations and annotations