Turns a declaration into a html note structure.

def PhysLean.NoteFile.sortLE (N : NoteFile) (ni1 ni2 : HTMLNote) : Bool

Sorts NoteInfo's by file name then by line number.

Equations

• One or more equations did not get rendered due to their size.

unsafe def PhysLean.NoteFile.getNodeInfo (N : NoteFile) : Lean.CoreM (List HTMLNote)

Returns a sorted list of NodeInfos for a file system.

Equations

• One or more equations did not get rendered due to their size.

def PhysLean.NoteFile.codeBlockHTML : String

The HTML code needed to have syntax highlighting.

Equations

• One or more equations did not get rendered due to their size.

def PhysLean.NoteFile.informalDefStyle : String

The html styles for informal definitions.

Equations

• One or more equations did not get rendered due to their size.

def PhysLean.NoteFile.codeButton : String

The html styles for code button.

Equations

• One or more equations did not get rendered due to their size.

def PhysLean.NoteFile.mathJaxScript : String

HTML allowing the use of mathjax.

Equations

• One or more equations did not get rendered due to their size.

def PhysLean.NoteFile.headerHTML : String

The header to the html code.

Equations

• One or more equations did not get rendered due to their size.

def PhysLean.NoteFile.titleHTML (N : NoteFile) : String

The html code corresponding to the title, abstract and authors.

Equations

• One or more equations did not get rendered due to their size.

def PhysLean.NoteFile.leanNote : String

The html code corresponding to a note about Lean and its use.

Equations

• One or more equations did not get rendered due to their size.

def PhysLean.NoteFile.footerHTML : String

The footer of the html file.

Equations

• PhysLean.NoteFile.footerHTML = "</body>\n</html>"

unsafe def PhysLean.NoteFile.toHTMLString (N : NoteFile) : Lean.MetaM String

The html file associated to a NoteFile string.

Equations

• One or more equations did not get rendered due to their size.