Turns a delaration into a html note structure.

structure PhysLean.HTMLNote : Type

A HTMLNote is a structure containing the html information from individual contributions (commands, informal commands, note ..) etc. to a note file.

• fileName : Lean.Name

  The name of the file the contribution came from.

• content : String

  The html contribution of the content.

• line : Nat

  The line in the file where the contribution came from.

def PhysLean.HTMLNote.ofNodeInfo (ni : NoteInfo) : HTMLNote

Converts a note info into a HTMLNote.

Equations

• PhysLean.HTMLNote.ofNodeInfo ni = { fileName := ni.fileName, content := ni.content, line := ni.line }

def PhysLean.HTMLNote.ofFormal (name : Lean.Name) : Lean.CoreM HTMLNote

An formal definition or lemma to html for a note.

Equations

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

unsafe def PhysLean.HTMLNote.ofInformal (name : Lean.Name) : Lean.CoreM HTMLNote

An informal definition or lemma to html for a note.

Equations

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