Merge pull request #156 from HEPLean/informal_defs

docs: Add informal def and proof to website

docs/_layouts/default.html

@@ -28,6 +28,7 @@
         <a href="{{ site.github.tar_url }}" class="btn">Download .tar.gz</a>
       {% endif %}
       <a href="https://heplean.github.io/HepLean/TODOList" class="btn">TODO List</a>
+      <a href="https://heplean.github.io/HepLean/Informal.html" class="btn">Help formalize</a>
     </header>
 
     <main id="content" class="main-content" role="main">
@@ -41,4 +42,4 @@
       </footer>
     </main>
   </body>
-</html>
+</html>

scripts/MetaPrograms/informal.lean

@@ -142,6 +142,8 @@ unsafe def informalToWebString (c : Import × ConstantInfo) : MetaM String := do
 def informalFileHeader : String := s!"
 # Informal definitions and lemmas
 
+See [informal definitions and lemmas as a dependency graph](https://heplean.github.io/HepLean/graph.svg).
+
 This file is automatically generated using `informal_lemma` and `informal_definition` commands
 appearing in the raw Lean code of HepLean.