Basic Lean meta programming commands

def Array.flatSize {α : Type u_1} : Array (Array α) → Nat

The size of a flattened array of arrays.

Equations

• as.flatSize = Array.foldl (fun (sizeAcc : Nat) (as : Array α) => sizeAcc + as.size) 0 as

def Array.flatFilterSizeM {α : Type} {m : Type → Type u_1} [Monad m] (p : α → m Bool) : Array (Array α) → m Nat

The size of a flattened array of arrays after applying an element-wise filter.

Equations

• Array.flatFilterSizeM p as = Array.foldlM (fun (sizeAcc : Nat) (as : Array α) => do let __do_lift ← Array.filterM p as pure (sizeAcc + __do_lift.size)) 0 as

Imports

def PhysLean.allImports : IO (Array Lean.Import)

Gets all imports within PhysLean.

Equations

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

def PhysLean.noImports : IO Nat

Number of files within PhysLean.

Equations

• PhysLean.noImports = do let imports ← PhysLean.allImports pure imports.size

def PhysLean.Imports.getConsts (imp : Lean.Import) : IO (Array Lean.ConstantInfo)

Gets all constants from an import.

Equations

• PhysLean.Imports.getConsts imp = do let mFile ← Lean.findOLean imp.module let __discr ← Lean.readModuleData mFile match __discr with | (modData, snd) => pure modData.constants

def PhysLean.Imports.getUserConsts (imp : Lean.Import) : Lean.CoreM (Array Lean.ConstantInfo)

Gets all user defined constants from an import.

Equations

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

def Lean.Name.toFilePath (c : Name) : System.FilePath

Turns a name into a system file path.

Equations

• c.toFilePath = (System.mkFilePath (c.toString.splitOn ".")).addExtension "lean"

def PhysLean.Imports.getLines (imp : Lean.Import) : IO (Array String)

Lines from import.

Equations

• PhysLean.Imports.getLines imp = IO.FS.lines imp.module.toFilePath

Name

def Lean.Name.toRelativeFilePath (c : Name) : System.FilePath

Turns a name into a Lean file.

Equations

• c.toRelativeFilePath = { toString := "." }.join c.toFilePath

def Lean.Name.toGitHubLink (c : Name) (line : Nat) : String

Turns a name, which represents a module, into a link to github.

Equations

• c.toGitHubLink line = toString "https://github.com/HEPLean/PhysLean/blob/master/" ++ toString c.toFilePath ++ toString "#L" ++ toString line ++ toString ""

def Lean.Name.lineNumber {m : Type → Type} [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] (c : Name) : m Nat

Given a name, returns the line number.

Equations

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

def Lean.Name.fileName {m : Type → Type} [Monad m] [MonadEnv m] (c : Name) : m Name

Given a name, returns the file name corresponding to that declaration.

Equations

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

def Lean.Name.location {m : Type → Type} [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] (c : Name) : m String

Returns the location of a name.

Equations

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

def Lean.Name.hasPos {m : Type → Type} [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] (c : Name) : m Bool

Determines if a name has a location.

Equations

• c.hasPos = do let ranges? ← Lean.findDeclarationRanges? c pure ranges?.isSome

def Lean.Name.hasDocString (c : Name) : CoreM Bool

Determines if a name has a doc string.

Equations

• c.hasDocString = do let env ← Lean.getEnv let doc? ← liftM (Lean.findDocString? env c) pure doc?.isSome

def Lean.Name.getDocString (c : Name) : CoreM String

The doc string from a name.

Equations

• c.getDocString = do let env ← Lean.getEnv let doc? ← liftM (Lean.findDocString? env c) pure (doc?.getD "")

def Lean.Name.getDeclString (name : Name) : CoreM String

Given a name, returns the source code defining that name, including doc strings.

Equations

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

def Lean.Name.getDeclStringNoDoc (name : Name) : CoreM String

Given a name, returns the source code defining that name, starting with the def ... or lemma... etc.

Equations

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

def PhysLean.noDefs : Lean.CoreM Nat

Number of definitions.

Equations

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

def PhysLean.noLemmas : Lean.CoreM Nat

Number of definitions.

Equations

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

def PhysLean.allDocStrings : Lean.CoreM (Array String)

All docstrings present in PhysLean.

Equations

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

def PhysLean.noDefsNoDocString : Lean.CoreM Nat

Number of definitions without a doc-string.

Equations

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

def PhysLean.noLemmasNoDocString : Lean.CoreM Nat

Number of definitions without a doc-string.

Equations

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

def PhysLean.noLines : IO Nat

The number of lines in PhysLean.

Equations

• PhysLean.noLines = do let imports ← PhysLean.allImports let x ← Array.mapM PhysLean.Imports.getLines imports pure x.flatSize

def PhysLean.noTODOs : IO Nat

The number of TODO items.

Equations

• PhysLean.noTODOs = do let imports ← PhysLean.allImports let x ← Array.mapM PhysLean.Imports.getLines imports Array.flatFilterSizeM (fun (l : String) => pure (l.startsWith "TODO ")) x

def PhysLean.noFilesWithTODOs : IO Nat

The number of files with a TODO item.

Equations

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