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

docs: Add informal def and proof to website

Browse source
This commit is contained in:
jstoobysmith 2024-09-17 10:03:02 -04:00
parent 364d5fbe6f
commit 2d8a16cc09
2 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
scripts/MetaPrograms/informal.lean
View file

@ -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.