DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Update informal.lean

Browse source
This commit is contained in:
jstoobysmith 2024-09-29 15:14:59 +00:00
parent d5691db8c8
commit 6c39e39273
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
scripts/MetaPrograms/informal.lean
View file

@ -414,7 +414,9 @@ unsafe def toHTML (imports : Array Import) : MetaM String := do
<!-- Add a title to the page -->
<h1 style=\"text-align: center;\">Informal dependency graph for HepLean</h1>
<p style=\"text-align: center;\">Click on a node to display the text associated with it.</p>
<p style=\"text-align: center;\">This graph only shows informal results (gray) and their direct formal dependencies (blue).
It does not show all results formalised into HepLean.</p>
<!-- Div to display the graph -->
<div id=\"graph\" style=\"width: 100vw; height: 75vh; border: 1px solid black\"></div>