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

feat: update Links

Browse source
This commit is contained in:
jstoobysmith 2024-12-05 07:12:56 +00:00
parent 84b328f13f
commit a5c72fe32c
2 changed files with 9 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
HepLean/Meta/Notes/HTMLNote.lean
View file

@ -45,11 +45,12 @@ unsafe def HTMLNote.ofInformal (name : Name) : MetaM HTMLNote := do
let line ← Name.lineNumber name
let fileName ← Name.fileName name
let constInfo ← getConstInfo name
let webAddress : String ← Name.toGitHubLink fileName line
let mut content := ""
if Informal.isInformalDef constInfo then
let X ← Informal.constantInfoToInformalDefinition constInfo
content := "<div class=\"informal-def\">"
++ "<a href=\"https://example.com\" class=\"button\">Improve/Formalize</a>"
++ "<a href=\"" ++ webAddress ++ "\" class=\"button\">Improve/Formalize</a>"
++"<b>Informal definition:</b> " ++ name.toString ++ "<br>"
++ X.math.replace "\n" "<br>"
++ "</div>"