Spaces:
Running
Running
Update server.py
Browse files
server.py
CHANGED
@@ -64,6 +64,9 @@ def read_root():
|
|
64 |
<button type="submit" class="bg-green-700 text-white p-2 w-24 rounded-lg">Search</button>
|
65 |
</form>
|
66 |
<ul id="results" class="list-disc">
|
|
|
|
|
|
|
67 |
</ul>
|
68 |
<script>
|
69 |
function removeFirstWord(str) {
|
|
|
64 |
<button type="submit" class="bg-green-700 text-white p-2 w-24 rounded-lg">Search</button>
|
65 |
</form>
|
66 |
<ul id="results" class="list-disc">
|
67 |
+
<div>You can search for any object declared in Mathlib and Lean, including theorems, functions, types, syntax, tactics, and metaprogramming functions.</div>
|
68 |
+
<div>The neural network sees the name, type, file location, and comment of a declaration. Your search terms should match these as closely as possible. </div>
|
69 |
+
<div>You can find README.md and the code I used in the Files tab. Thank you!</div>
|
70 |
</ul>
|
71 |
<script>
|
72 |
function removeFirstWord(str) {
|