mathlib documentation

tactic.protected

protected and protect_proj user attributes #

protected is an attribute to protect a declaration. If a declaration foo.bar is marked protected, then it must be referred to by its full name foo.bar, even when the foo namespace is open.

protect_proj attribute to protect the projections of a structure. If a structure foo is marked with the protect_proj user attribute, then all of the projections become protected.

protect_proj without bar baz will protect all projections except for bar and baz.

Examples #

In this example all of foo.bar, foo.baz and foo.qux will be protected.

@[protect_proj] structure foo : Type :=
(bar : unit) (baz : unit) (qux : unit)

The following code example define the structure foo, and the projections foo.qux will be protected, but not foo.baz or foo.bar

@[protect_proj without baz bar] structure foo : Type :=
(bar : unit) (baz : unit) (qux : unit)
source
meta def tactic.protected_attr  :
(user_attribute unit)

Attribute to protect a declaration. If a declaration foo.bar is marked protected, then it must be referred to by its full name foo.bar, even when the foo namespace is open.

Protectedness is a built in parser feature that is independent of this attribute. A declaration may be protected even if it does not have the @[protected] attribute. This provides a convenient way to protect many declarations at once.

source
meta def tactic.protect_proj_tac (n : name) (l : list name) :
tactic unit

Tactic that is executed when a structure is marked with the protect_proj attribute

source
meta def tactic.protect_proj_attr  :
user_attribute unit (list name)

Attribute to protect the projections of a structure. If a structure foo is marked with the protect_proj user attribute, then all of the projections become protected, meaning they must always be referred to by their full name foo.bar, even when the foo namespace is open.

protect_proj without bar baz will protect all projections except for bar and baz.

@[protect_proj without baz bar] structure foo : Type :=
(bar : unit) (baz : unit) (qux : unit)