1. Physlib
  2. Meta
  3. Notes
  4. NoteFile
Imports
/- Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ module public import Lean.Setup

Note file

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

@[expose] public section

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

The overall title of the note.

The abstract of the note.

A list of authors.

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

structure NoteFile where title : String abstract : String authors : List String files : List Name

All imports associated to a note.

def imports : Array Import := (N.files.map fun f => {module := f}).toArray