Documentation

Lean.EnvExtension

Further environment extension API; the primitives live in Lean.Environment.

Simple PersistentEnvExtension that implements exportEntriesFn using a list of entries.

Equations
Instances For
    @[specialize #[]]
    def Lean.mkStateFromImportedEntries {α σ : Type} (addEntryFn : σασ) (initState : σ) (as : Array (Array α)) :
    σ
    Equations
    Instances For
      • name : Name
      • addEntryFn : σασ
      • addImportedFn : Array (Array α)σ
      • toArrayFn : List αArray α
      • replay? : Option (List ασσList α × σ)
      • exported : Bool

        Whether entries should be imported into other modules. Entries are always accessible in the language server via getModuleEntries (includeServer := true).

      Instances For
        def Lean.SimplePersistentEnvExtension.replayOfFilter {σ : Type u_1} {α : Type u_2} (p : σαBool) (addEntryFn : σασ) :
        List ασσList α × σ

        Returns a function suitable for SimplePersistentEnvExtensionDescr.replay? that replays all new entries onto the state using addEntryFn. p should filter out entries that have already been added to the state by a prior replay of the same realizable constant.

        Equations
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            Get the list of values used to update the state of the given SimplePersistentEnvExtension in the current file.

            Equations
            Instances For

              Get the current state of the given SimplePersistentEnvExtension.

              Equations
              Instances For

                Set the current state of the given SimplePersistentEnvExtension. This change is not persisted across files.

                Equations
                Instances For

                  Modify the state of the given extension in the given environment by applying the given function. This change is not persisted across files.

                  Equations
                  Instances For

                    Returns the final extension state on the environment branch corresponding to the passed declaration name, if any, or otherwise the state on the current branch. In other words, at most one environment branch will be blocked on.

                    Equations
                    Instances For

                      Environment extension for tagging declarations. Declarations must only be tagged in the module where they were declared.

                      Equations
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For

                              Environment extension for mapping declarations to values. Declarations must only be inserted into the mapping in the module where they were declared.

                              Instances For
                                def Lean.mkMapDeclarationExtension {α : Type} (name : Name := by exact decl_name%) (exportEntriesFn : NameMap αArray (Name × α) := fun (x : NameMap α) => RBMap.toArray x) :
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  def Lean.MapDeclarationExtension.insert {α : Type} (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) (val : α) :
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    def Lean.MapDeclarationExtension.find? {α : Type} [Inhabited α] (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) (includeServer : Bool := false) :
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For