Note file

A note file is a structure which contains the information to go into a note.

structure PhysLean.NoteFile : Type

A note consists of a title and a list of Lean files which make up the note.

• title : String

  The overall title of the note.

• abstract : String

  The abstract of the note.

• authors : List String

  A list of authors.

• files : List Lean.Name

  The files making up the note in the order in which they should appear.

def PhysLean.NoteFile.imports (N : NoteFile) : Array Lean.Import

All imports associated to a note.

Equations

• N.imports = (List.map (fun (f : Lean.Name) => { module := f, runtimeOnly := false }) N.files).toArray