diff --git a/scripts/MetaPrograms/informal.lean b/scripts/MetaPrograms/informal.lean index 2c6cbd2..7777ca3 100644 --- a/scripts/MetaPrograms/informal.lean +++ b/scripts/MetaPrograms/informal.lean @@ -414,7 +414,9 @@ unsafe def toHTML (imports : Array Import) : MetaM String := do

Informal dependency graph for HepLean

- +

Click on a node to display the text associated with it.

+

This graph only shows informal results (gray) and their direct formal dependencies (blue). + It does not show all results formalised into HepLean.