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

doc: Informal graph arrows

Browse source
This commit is contained in:
jstoobysmith 2024-09-17 11:54:32 -04:00
parent 3271417b37
commit 62f1153088
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
scripts/MetaPrograms/informal.lean
View file

@ -265,7 +265,8 @@ unsafe def mkDot (imports : Array Import) : MetaM String := do
bgcolor=\"lightyellow\";
label=\"Informal dependency graph for HepLean\";
labelloc=\"t\";
labeljust=\"l\";"
labeljust=\"l\";
edge [arrowhead=vee];"
let footer := "}"
let nodes := String.intercalate "\n" formal_nodes.toList
let informalLemmaNodes ← informal.mapM informalToNode