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-16 10:11:25 -04:00
parent 41ec9f5805
commit 6713e2f86d
1 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

7
scripts/MetaPrograms/informal.lean
View file

@ -131,6 +131,13 @@ unsafe def informalToWebString (c : Import × ConstantInfo) : MetaM String := do
def informalFileHeader : String := s!"
# Informal definitions and lemmas
This file is automatically generated using `informal_lemma` and `informal_definition` commands
appearing in the raw Lean code of HepLean.
There is an implicit invitation to the reader to contribute to the formalization of
informal definitions and lemmas. You may also wish to contribute to HepLean by including
informal definitions and lemmas in the raw Lean code, especially if you do not have a
background in Lean.
"