instruct the compiler that function applications using the tagged declaration should not be extracted when they are closed terms, nor common subexpression should be performed. This is useful for declarations that have implicit effects.


docstring code block suggestion provider


inherit documentation from a specified declaration


(builtin) adds a syntax traversal for the missing docs linter


(builtin) Register a parenthesizer for a parser.


instructs elaborator that the arguments of the function application should be elaborated as were an eliminator


custom `rec`-like eliminator for the `induction` tactic


custom `casesOn`-like eliminator for the `cases` tactic


simp lemma used in the preprocessing of well-founded recursive function definitions, in particular to add additional hypotheses to the context. Also see `wfParam`.


Registers a custom name for a tactic. This custom name should be a prefix of the tactic's syntax, because it is used in completion.


Register a formatter for a parser combinator


eqns

Overrides the equation lemmas for a declaration to the provided list


mark that a definition can be used in a pattern (remark: the dependent pattern matching compiler will unfold the definition)


The `push_cast` simp attribute uses `norm_cast` lemmas to move casts toward the leaf nodes of the expression.


nolint

Do not report this declaration in any of the tests of `#lint`


recursor

user defined recursor, numerical parameter specifies position of the major premise


simp theorems used to convert UIntX/IntX statements into BitVec ones


generate the `.toCtorIdx` and `.ctor.elim` definitions for the given inductive


expose

(module system) Make bodies of definitions available to importing modules.


Use to decorate methods for suggesting code actions. This is a low-level interface for making code actions.


defeq

mark theorem as a definitional equality, to be used by `dsimp`


An attribute specifying that this is a notation class. Used by @[simps].


adds a syntax traversal for the missing docs linter


simp theorems used by internal DTreeMap lemmas


Declare a new command code action, to appear in the code actions on commands


(module system) Negate previous `[expose]` attribute.


auxiliary definition used to implement coercion (unfolded during elaboration)


Declare a new hole code action, to appear in the code actions on ?_ and _


Declare a new builtin command code action, to appear in the code actions on commands


Register a double backtick syntax quotation pre-check.


ext

Marks a theorem as an extensionality theorem


(builtin) Marks a function of type `Lean.Linter.IgnoreFunction` for suppressing unused variable warnings


(builtin) Register a formatter for a parser.


mark structure to be pretty printed using `⟨a,b,c⟩` notation


spec

Marks Hoare triple specifications and simp theorems to use with the `mspec` and `mvcgen` tactics


(builtin) Register an elaborator for inductive types


simps

Automatically derive lemmas specifying the projections of this declaration.


mark declaration to never be pretty printed using field notation


initialization procedure for global references


suggest other (incorrect, not-existing) identifiers that someone might use when they actually want this definition


mark definition to always be inlined before ANF conversion


docstring code element suggestion provider


Register an unexpander for applications of a given constant.


specialize

mark definition to always be specialized


simp lemmas converting `BitVec` goals to `Nat` goals


grind!?

The `[grind!?]` attribute is identical to the `[grind!]` attribute, but displays inferred pattern information.When applied to an equational theorem, `[grind =]`, `[grind =_]`, or `[grind _=_]`will mark the theorem for use in heuristic instantiations by the `grind` tactic,
      using respectively the left-hand side, the right-hand side, or both sides of the theorem.When applied to a function, `[grind =]` automatically annotates the equational theorems associated with that function.When applied to a theorem `[grind ←]` will instantiate the theorem whenever it encounters the conclusion of the theorem
      (that is, it will use the theorem for backwards reasoning).When applied to a theorem `[grind →]` will instantiate the theorem whenever it encounters sufficiently many of the propositional hypotheses
      (that is, it will use the theorem for forwards reasoning).The attribute `[grind]` by itself will effectively try `[grind ←]` (if the conclusion is sufficient for instantiation) and then `[grind →]`.The `grind` tactic utilizes annotated theorems to add instances of matching patterns into the local context during proof search.For example, if a theorem `@[grind =] theorem foo_idempotent : foo (foo x) = foo x` is annotated,`grind` will add an instance of this theorem to the local context whenever it encounters the pattern `foo (foo x)`.


(builtin) Use to decorate methods for suggesting code actions. This is a low-level interface for making code actions.


Registers a widget module. Its type must implement Lean.Widget.ToModule.


Auxiliary attribute for `to_additive` stating that certain arguments are not additivized.


Register a parenthesizer for a parser combinator.


name of the Lean (probably unsafe) function that implements opaque constant


Marks a function as a Lean server RPC method.
    Shorthand for `registerRpcProcedure`.
    The function must have type `α → RequestM (RequestTask β)` with
    `[RpcEncodable α]` and `[RpcEncodable β]`.


Auxiliary attribute for `to_additive` stating that the operations on this type should not be translated.


Register an elaborator for inductive types


Use this declaration as a linting test in #lint


(builtin) Register a parenthesizer for a syntax category.


Auxiliary attribute for `to_additive` stating that the operations on this type should be translated.


Register a tactic parser as an alternative form of an existing tactic, so they can be grouped together in documentation.


make the docs and location of this declaration available as a builtin


mark that applications of the given declaration should be elaborated without the expected type


unbox

compiler tries to unbox result values if their types are tagged with `[unbox]`


grind

The `[grind]` attribute is used to annotate declarations.When applied to an equational theorem, `[grind =]`, `[grind =_]`, or `[grind _=_]`will mark the theorem for use in heuristic instantiations by the `grind` tactic,
      using respectively the left-hand side, the right-hand side, or both sides of the theorem.When applied to a function, `[grind =]` automatically annotates the equational theorems associated with that function.When applied to a theorem `[grind ←]` will instantiate the theorem whenever it encounters the conclusion of the theorem
      (that is, it will use the theorem for backwards reasoning).When applied to a theorem `[grind →]` will instantiate the theorem whenever it encounters sufficiently many of the propositional hypotheses
      (that is, it will use the theorem for forwards reasoning).The attribute `[grind]` by itself will effectively try `[grind ←]` (if the conclusion is sufficient for instantiation) and then `[grind →]`.The `grind` tactic utilizes annotated theorems to add instances of matching patterns into the local context during proof search.For example, if a theorem `@[grind =] theorem foo_idempotent : foo (foo x) = foo x` is annotated,`grind` will add an instance of this theorem to the local context whenever it encounters the pattern `foo (foo x)`.


builtin docstring code block suggestion provider


simp lemmas converting boolean expressions in terms of `decide` into propositional statements


mark definition to be inlined when resultant term after reduction is not a `cases_on` application


docstring code element suggestion provider


incremental

Marks an elaborator (tactic or command, currently) as supporting incremental elaboration. For unmarked elaborators, the corresponding snapshot bundle field in the elaboration context is unset so as to prevent accidental, incorrect reuse.


Register a parenthesizer for a syntax category.


explicitly run hooks normally activated by builtin parser attributes


(builtin) Marks an elaborator (tactic or command, currently) as supporting incremental elaboration. For unmarked elaborators, the corresponding snapshot bundle field in the elaboration context is unset so as to prevent accidental, incorrect reuse.


simp theorems internally used by `mvcgen`


grind!

The `[grind!]` attribute is used to annotate declarations, but selecting minimal indexable subterms.When applied to an equational theorem, `[grind =]`, `[grind =_]`, or `[grind _=_]`will mark the theorem for use in heuristic instantiations by the `grind` tactic,
      using respectively the left-hand side, the right-hand side, or both sides of the theorem.When applied to a function, `[grind =]` automatically annotates the equational theorems associated with that function.When applied to a theorem `[grind ←]` will instantiate the theorem whenever it encounters the conclusion of the theorem
      (that is, it will use the theorem for backwards reasoning).When applied to a theorem `[grind →]` will instantiate the theorem whenever it encounters sufficiently many of the propositional hypotheses
      (that is, it will use the theorem for forwards reasoning).The attribute `[grind]` by itself will effectively try `[grind ←]` (if the conclusion is sufficient for instantiation) and then `[grind →]`.The `grind` tactic utilizes annotated theorems to add instances of matching patterns into the local context during proof search.For example, if a theorem `@[grind =] theorem foo_idempotent : foo (foo x) = foo x` is annotated,`grind` will add an instance of this theorem to the local context whenever it encounters the pattern `foo (foo x)`.


grind?

The `[grind?]` attribute is identical to the `[grind]` attribute, but displays inferred pattern information.When applied to an equational theorem, `[grind =]`, `[grind =_]`, or `[grind _=_]`will mark the theorem for use in heuristic instantiations by the `grind` tactic,
      using respectively the left-hand side, the right-hand side, or both sides of the theorem.When applied to a function, `[grind =]` automatically annotates the equational theorems associated with that function.When applied to a theorem `[grind ←]` will instantiate the theorem whenever it encounters the conclusion of the theorem
      (that is, it will use the theorem for backwards reasoning).When applied to a theorem `[grind →]` will instantiate the theorem whenever it encounters sufficiently many of the propositional hypotheses
      (that is, it will use the theorem for forwards reasoning).The attribute `[grind]` by itself will effectively try `[grind ←]` (if the conclusion is sufficient for instantiation) and then `[grind →]`.The `grind` tactic utilizes annotated theorems to add instances of matching patterns into the local context during proof search.For example, if a theorem `@[grind =] theorem foo_idempotent : foo (foo x) = foo x` is annotated,`grind` will add an instance of this theorem to the local context whenever it encounters the pattern `foo (foo x)`.


mark extern definition to always return tagged values


(builtin) Register a double backtick syntax quotation pre-check.


simp lemma used to post-process the theorem created by `@[method_specs]`.


Marks a function as a computed field of an inductive


Marks a function of type `Lean.Linter.IgnoreFunction` for suppressing unused variable warnings


explicitly run hooks normally activated by parser attributes


Register a tactic suggestion generator for try? (runs after built-in tactics)


(builtin) Registers a widget module. Its type must implement Lean.Widget.ToModule.


Register a tactic parser as an alternative of an existing tactic, so they can be grouped together in documentation.