Physlib.Meta.Notes.HTMLNote

Given a structure $ni$ of type `NoteInfo` containing information about a declaration or note, this function converts it into an `HTMLNote` structure.

Given a formal declaration name $c$, this function constructs an `HTMLNote` structure within the `CoreM` monad. It retrieves the line number $n$, the file name, and the literal source code string associated with $c$ from the environment. The function generates an HTML block containing: 1. A GitHub link to the source code at line $n$ within the `physlib` repository. 2. The source code of the declaration $c$ (retrieved via `getDeclString`) enclosed in HTML `<pre><code>` tags for display. The resulting `HTMLNote` object includes this formatted HTML content along with the source file and line number metadata.

Given a declaration name $c$, this function constructs an `HTMLNote` structure within the `CoreM` monad. It retrieves the line number $n$, the file name, and the documentation string associated with $c$ from the environment. Based on whether the declaration is an `InformalDefinition` or an `InformalLemma`, the function generates an HTML block containing: 1. A GitHub link to the source code at line $n$. 2. The name of the declaration $c$. 3. The contents of the documentation string, where newlines are replaced by HTML line breaks. The resulting `HTMLNote` includes this formatted HTML content along with the source file metadata.