doc-next-gen

Init.MetaTypes

Module docstring

{}

Lean.NameGenerator structure
Full source 
structure NameGenerator where
  namePrefix : Name := `_uniq
  idx        : Nat  := 1
  deriving Inhabited
Lean Name Generator
Informal description
The structure `Lean.NameGenerator` represents a generator for creating fresh names in the Lean theorem prover. It is used to produce unique identifiers during proof automation and other metaprogramming tasks.
Lean.instInhabitedNameGenerator instance
: Inhabited✝ (@Lean.NameGenerator)
Full source 
Inhabited
Inhabited Type of Lean Name Generators
Informal description
The type `Lean.NameGenerator` is inhabited, meaning it has a designated default element.
Lean.Module structure
Full source 
/-- Syntax objects for a Lean module. -/
structure Module where
  header   : Syntax
  commands : Array Syntax
Lean Module Structure
Informal description
The structure representing a Lean module, which contains syntax objects and related components for organizing Lean code.
Lean.Meta.TransparencyMode inductive
Full source 
/--
Which constants should be unfolded?
-/
inductive TransparencyMode where
  /-- Unfolds all constants, even those tagged as `@[irreducible]`. -/
  | all
  /-- Unfolds all constants except those tagged as `@[irreducible]`. -/
  | default
  /-- Unfolds only constants tagged with the `@[reducible]` attribute. -/
  | reducible
  /-- Unfolds reducible constants and constants tagged with the `@[instance]` attribute. -/
  | instances
  deriving Inhabited, BEq
Transparency modes in Lean metaprogramming
Informal description
An inductive type representing different modes of constant unfolding in Lean's metaprogramming environment. These modes determine which constants should be unfolded during various metaprogramming operations.
Lean.Meta.instInhabitedTransparencyMode instance
: Inhabited✝ (@Lean.Meta.TransparencyMode)
Full source 
Inhabited, BEq
Inhabited Transparency Mode in Lean Metaprogramming
Informal description
The type `Lean.Meta.TransparencyMode` is inhabited, meaning it has a default element.
Lean.Meta.instBEqTransparencyMode instance
: BEq✝ (@Lean.Meta.TransparencyMode✝)
Full source 
BEq
Boolean Equality on Transparency Modes
Informal description
The type `Lean.Meta.TransparencyMode` is equipped with a boolean equality relation `==`.
Lean.Meta.EtaStructMode inductive
Full source 
/-- Which structure types should eta be used with? -/
inductive EtaStructMode where
  /-- Enable eta for structure and classes. -/
  | all
  /-- Enable eta only for structures that are not classes. -/
  | notClasses
  /-- Disable eta for structures and classes. -/
  | none
  deriving Inhabited, BEq
Eta reduction mode for structures
Informal description
An inductive type representing different modes for determining which structure types should use eta reduction (η-reduction) in the Lean metaprogramming framework. Eta reduction is a process that simplifies terms of the form `(fun x => f x)` to `f` when `x` is not free in `f`.
Lean.Meta.instInhabitedEtaStructMode instance
: Inhabited✝ (@Lean.Meta.EtaStructMode)
Full source 
Inhabited, BEq
Default Element for Eta Reduction Mode
Informal description
The type `Lean.Meta.EtaStructMode` has a default element.
Lean.Meta.instBEqEtaStructMode instance
: BEq✝ (@Lean.Meta.EtaStructMode✝)
Full source 
BEq
Boolean Equality on Eta Reduction Mode
Informal description
The type `Lean.Meta.EtaStructMode` is equipped with a boolean equality relation `==`.
Lean.Meta.DSimp.Config structure
Full source 
/--
The configuration for `dsimp`.
Passed to `dsimp` using, for example, the `dsimp (config := {zeta := false})` syntax.

Implementation note: this structure is only used for processing the `(config := ...)` syntax, and it is not used internally.
It is immediately converted to `Lean.Meta.Simp.Config` by `Lean.Elab.Tactic.elabSimpConfig`.
-/
structure Config where
  /--
  When `true` (default: `true`), performs zeta reduction of let expressions.
  That is, `let x := v; e[x]` reduces to `e[v]`.
  See also `zetaDelta`.
  -/
  zeta              : Bool := true
  /--
  When `true` (default: `true`), performs beta reduction of applications of `fun` expressions.
  That is, `(fun x => e[x]) v` reduces to `e[v]`.
  -/
  beta              : Bool := true
  /--
  TODO (currently unimplemented). When `true` (default: `true`), performs eta reduction for `fun` expressions.
  That is, `(fun x => f x)` reduces to `f`.
  -/
  eta               : Bool := true
  /--
  Configures how to determine definitional equality between two structure instances.
  See documentation for `Lean.Meta.EtaStructMode`.
  -/
  etaStruct         : EtaStructMode := .all
  /--
  When `true` (default: `true`), reduces `match` expressions applied to constructors.
  -/
  iota              : Bool := true
  /--
  When `true` (default: `true`), reduces projections of structure constructors.
  -/
  proj              : Bool := true
  /--
  When `true` (default: `false`), rewrites a proposition `p` to `True` or `False` by inferring
  a `Decidable p` instance and reducing it.
  -/
  decide            : Bool := false
  /--
  When `true` (default: `false`), unfolds definitions.
  This can be enabled using the `simp!` syntax.
  -/
  autoUnfold        : Bool := false
  /--
  If `failIfUnchanged` is `true` (default: `true`), then calls to `simp`, `dsimp`, or `simp_all`
  will fail if they do not make progress.
  -/
  failIfUnchanged   : Bool := true
  /--
  If `unfoldPartialApp` is `true` (default: `false`), then calls to `simp`, `dsimp`, or `simp_all`
  will unfold even partial applications of `f` when we request `f` to be unfolded.
  -/
  unfoldPartialApp  : Bool := false
  /--
  When `true` (default: `false`), local definitions are unfolded.
  That is, given a local context containing entry `x : t := e`, the free variable `x` reduces to `e`.
  -/
  zetaDelta         : Bool := false
  /--
  When `index` (default : `true`) is `false`, `simp` will only use the root symbol
  to find candidate `simp` theorems. It approximates Lean 3 `simp` behavior.
  -/
  index             : Bool := true
  /--
  When `true` (default : `true`), then simps will remove unused let-declarations:
  `let x := v; e` simplifies to `e` when `x` does not occur in `e`.
  -/
  zetaUnused : Bool := true
  deriving Inhabited, BEq
Configuration for the `dsimp` tactic
Informal description
The structure `Lean.Meta.DSimp.Config` represents the configuration options for the `dsimp` tactic in Lean. This configuration is used to control various aspects of the simplification process, such as whether to perform zeta-reduction (simplification of let-bindings). The structure is primarily used for processing the `(config := ...)` syntax in tactic invocations and is not used internally; it is immediately converted to `Lean.Meta.Simp.Config`.
Lean.Meta.DSimp.instInhabitedConfig instance
: Inhabited✝ (@Lean.Meta.DSimp.Config)
Full source 
Inhabited, BEq
Default Configuration for `dsimp` Tactic
Informal description
The configuration structure `Lean.Meta.DSimp.Config` for the `dsimp` tactic is inhabited, meaning it has a default element.
Lean.Meta.DSimp.instBEqConfig instance
: BEq✝ (@Lean.Meta.DSimp.Config✝)
Full source 
BEq
Boolean Equality for DSimp Configuration
Informal description
The configuration structure `Lean.Meta.DSimp.Config` has a boolean equality relation `==` defined on it.
Lean.Meta.Simp.defaultMaxSteps definition
Full source 
def defaultMaxSteps := 100000
Default maximum steps for simp tactic
Informal description
The default maximum number of steps for the `simp` tactic is set to 100,000.
Lean.Meta.Simp.Config structure
Full source 
/--
The configuration for `simp`.
Passed to `simp` using, for example, the `simp (config := {contextual := true})` syntax.

See also `Lean.Meta.Simp.neutralConfig` and `Lean.Meta.DSimp.Config`.
-/
structure Config where
  /--
  The maximum number of subexpressions to visit when performing simplification.
  The default is 100000.
  -/
  maxSteps          : Nat  := defaultMaxSteps
  /--
  When simp discharges side conditions for conditional lemmas, it can recursively apply simplification.
  The `maxDischargeDepth` (default: 2) is the maximum recursion depth when recursively applying simplification to side conditions.
  -/
  maxDischargeDepth : Nat  := 2
  /--
  When `contextual` is true (default: `false`) and simplification encounters an implication `p → q`
  it includes `p` as an additional simp lemma when simplifying `q`.
  -/
  contextual        : Bool := false
  /--
  When true (default: `true`) then the simplifier caches the result of simplifying each subexpression, if possible.
  -/
  memoize           : Bool := true
  /--
  When `singlePass` is `true` (default: `false`), the simplifier runs through a single round of simplification,
  which consists of running pre-methods, recursing using congruence lemmas, and then running post-methods.
  Otherwise, when it is `false`, it iteratively applies this simplification procedure.
  -/
  singlePass        : Bool := false
  /--
  When `true` (default: `true`), performs zeta reduction of let expressions.
  That is, `let x := v; e[x]` reduces to `e[v]`.
  See also `zetaDelta`.
  -/
  zeta              : Bool := true
  /--
  When `true` (default: `true`), performs beta reduction of applications of `fun` expressions.
  That is, `(fun x => e[x]) v` reduces to `e[v]`.
  -/
  beta              : Bool := true
  /--
  TODO (currently unimplemented). When `true` (default: `true`), performs eta reduction for `fun` expressions.
  That is, `(fun x => f x)` reduces to `f`.
  -/
  eta               : Bool := true
  /--
  Configures how to determine definitional equality between two structure instances.
  See documentation for `Lean.Meta.EtaStructMode`.
  -/
  etaStruct         : EtaStructMode := .all
  /--
  When `true` (default: `true`), reduces `match` expressions applied to constructors.
  -/
  iota              : Bool := true
  /--
  When `true` (default: `true`), reduces projections of structure constructors.
  -/
  proj              : Bool := true
  /--
  When `true` (default: `false`), rewrites a proposition `p` to `True` or `False` by inferring
  a `Decidable p` instance and reducing it.
  -/
  decide            : Bool := false
  /--  When `true` (default: `false`), simplifies simple arithmetic expressions. -/
  arith             : Bool := false
  /--
  When `true` (default: `false`), unfolds definitions.
  This can be enabled using the `simp!` syntax.
  -/
  autoUnfold        : Bool := false
  /--
  When `true` (default: `true`) then switches to `dsimp` on dependent arguments
  if there is no congruence theorem that would allow `simp` to visit them.
  When `dsimp` is `false`, then the argument is not visited.
  -/
  dsimp             : Bool := true
  /--
  If `failIfUnchanged` is `true` (default: `true`), then calls to `simp`, `dsimp`, or `simp_all`
  will fail if they do not make progress.
  -/
  failIfUnchanged   : Bool := true
  /--
  If `ground` is `true` (default: `false`), then ground terms are reduced.
  A term is ground when it does not contain free or meta variables.
  Reduction is interrupted at a function application `f ...` if `f` is marked to not be unfolded.
  Ground term reduction applies `@[seval]` lemmas.
  -/
  ground            : Bool := false
  /--
  If `unfoldPartialApp` is `true` (default: `false`), then calls to `simp`, `dsimp`, or `simp_all`
  will unfold even partial applications of `f` when we request `f` to be unfolded.
  -/
  unfoldPartialApp  : Bool := false
  /--
  When `true` (default: `false`), local definitions are unfolded.
  That is, given a local context containing entry `x : t := e`, the free variable `x` reduces to `e`.
  -/
  zetaDelta         : Bool := false
  /--
  When `index` (default : `true`) is `false`, `simp` will only use the root symbol
  to find candidate `simp` theorems. It approximates Lean 3 `simp` behavior.
  -/
  index             : Bool := true
  /--
  If `implicitDefEqProofs := true`, `simp` does not create proof terms when the
  input and output terms are definitionally equal.
  -/
  implicitDefEqProofs : Bool := true
  /--
  When `true` (default : `true`), then simps will remove unused let-declarations:
  `let x := v; e` simplifies to `e` when `x` does not occur in `e`.
  -/
  zetaUnused : Bool := true
  deriving Inhabited, BEq
Simplifier Configuration
Informal description
The structure `Lean.Meta.Simp.Config` represents the configuration options for the `simp` tactic in Lean. This configuration can be passed to `simp` using syntax like `simp (config := {contextual := true})`. It controls various aspects of how the simplifier behaves during simplification.
Lean.Meta.Simp.instInhabitedConfig instance
: Inhabited✝ (@Lean.Meta.Simp.Config)
Full source 
Inhabited, BEq
Default Simplifier Configuration
Informal description
The simplifier configuration `Lean.Meta.Simp.Config` is inhabited, meaning it has a default configuration.
Lean.Meta.Simp.instBEqConfig instance
: BEq✝ (@Lean.Meta.Simp.Config✝)
Full source 
BEq
Boolean Equality for Simplifier Configuration
Informal description
The simplifier configuration `Lean.Meta.Simp.Config` has a boolean equality structure, providing a boolean-valued equality relation `==` on its instances.
Lean.Meta.Simp.ConfigCtx structure
extends Config
Full source 
structure ConfigCtx extends Config where
  contextual := true
Simplification Configuration Context
Informal description
The structure `ConfigCtx` extends the `Config` structure, providing additional context for simplification procedures in Lean's metaprogramming framework.
Lean.Meta.Simp.neutralConfig definition
: Simp.Config
Full source 
/--
A neutral configuration for `simp`, turning off all reductions and other built-in simplifications.
-/
def neutralConfig : Simp.Config := {
  zeta              := false
  beta              := false
  eta               := false
  iota              := false
  proj              := false
  decide            := false
  arith             := false
  autoUnfold        := false
  ground            := false
  zetaDelta         := false
  zetaUnused        := false
}
Neutral configuration for `simp` tactic
Informal description
The configuration `neutralConfig` for the `simp` tactic disables all built-in simplification procedures, including $\zeta$-reduction (let-binding expansion), $\beta$-reduction (lambda application), $\eta$-reduction (lambda extensionality), $\iota$-reduction (recursor reduction), projection reduction, decision procedures, arithmetic simplification, automatic unfolding, ground evaluation, $\zeta$-delta reduction (let-binding expansion with delta reduction), and unused let-binding elimination.
Lean.Meta.Simp.NormCastConfig structure
extends Simp.Config
Full source 
structure NormCastConfig extends Simp.Config where
    zeta := false
    beta := false
    eta  := false
    proj := false
    iota := false
Normalization of Casts Configuration
Informal description
The structure `NormCastConfig` extends the configuration for simplification (`Simp.Config`) with additional settings specific to normalizing casts in Lean's metaprogramming environment.
Lean.Meta.Occurrences inductive
Full source 
/-- Configuration for which occurrences that match an expression should be rewritten. -/
inductive Occurrences where
  /-- All occurrences should be rewritten. -/
  | all
  /-- A list of indices for which occurrences should be rewritten. -/
  | pos (idxs : List Nat)
  /-- A list of indices for which occurrences should not be rewritten. -/
  | neg (idxs : List Nat)
  deriving Inhabited, BEq
Occurrence specification for term rewriting
Informal description
The inductive type `Occurrences` represents configuration options for specifying which occurrences of a matching expression should be rewritten. It is used to control pattern matching behavior during term rewriting operations.
Lean.Meta.instInhabitedOccurrences instance
: Inhabited✝ (@Lean.Meta.Occurrences)
Full source 
Inhabited, BEq
Default Element for Occurrences Type
Informal description
The type `Lean.Meta.Occurrences` is inhabited, meaning it has a designated default element.
Lean.Meta.instBEqOccurrences instance
: BEq✝ (@Lean.Meta.Occurrences✝)
Full source 
BEq
Boolean Equality for Occurrences Type
Informal description
The type `Lean.Meta.Occurrences` is equipped with a boolean equality relation `==`.
Lean.Meta.instCoeListNatOccurrences instance
: Coe (List Nat) Occurrences
Full source 
instance : Coe (List Nat) Occurrences := ⟨.pos⟩
Coercion from List of Natural Numbers to Occurrences
Informal description
There is a canonical way to treat a list of natural numbers as an occurrence specification for term rewriting.