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
- If a user imports a module that is indexed by the server, the contents of the module is not changed
- After a user calculates the pretty-printed form of a premise, it will not be changed any more (because of caching)
The data of a new premise sent to the server, including name and a signature consisting of docstring and type.
Instances For
Equations
Equations
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
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)