Documentation

PremiseSelection.Premise

Here we define mechanisms that send new user-defined premises to the server.

The entire architecture is very WIP: it depends on several unreal assumptions

The data of a new premise sent to the server, including name and a signature consisting of docstring and type.

Instances For

    Returns kind (string) given constant (from declarations.lean)

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

      A reference holding a mapping from a user-defined premise name to Premise.fromName name (see Premise.fromName).

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

        Serialize a declaration into a Premise by pretty-printing the declaration docstring and signature.

        If useCache := true, this function is cached by fromNameCacheRef, so on the second time it is called on the same declaration, it reads the previously stored result instead of calculates the signature again. (TODO) This is just a temporary solution so that it is reasonable to call e.g. aesop (add unsafe (by hammer)) where hammer is called many times.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def Lean.PremiseSelection.Premise.fromNames (names : Array Name) (chunkSize : Nat) (useCache : Bool) :

          This is equivalent to names.mapM Premise.fromName, but it processes chunks in parallel.

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

            TODO: use the implementation of deny-list in https://github.com/leanprover/lean4/tree/mepo instead (once the branch is merged)