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 Physlib.allImports : IO (Array Lean.Import)

Gets all imports within Physlib.

Equations

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

def Physlib.noImports : IO Nat

Number of files within Physlib.

Equations

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

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

Gets all constants from an import.

Equations

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

def Physlib.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 Physlib.Imports.getLines (imp : Lean.Import) : IO (Array String)

Lines from import.

Equations

• Physlib.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/leanprover-community/physlib/blob/master/" ++ toString c.toFilePath ++ toString "#L" ++ toString line

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 __do_lift ← liftM (Lean.findInternalDocString? env c) pure __do_lift.isSome

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

The doc string from a name.

Equations

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

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 Physlib.noDefs : Lean.CoreM Nat

Number of definitions.

Equations

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

def Physlib.noLemmas : Lean.CoreM Nat

Number of definitions.

Equations

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

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

All docstrings present in Physlib.

Equations

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

def Physlib.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 Physlib.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 Physlib.noLines : IO Nat

The number of lines in Physlib.

Equations

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

def Physlib.noTODOs : IO Nat

The number of TODO items.

Equations

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

def Physlib.noFilesWithTODOs : IO Nat

The number of files with a TODO item.

Equations

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

def Physlib.allUserConsts : Lean.CoreM (Array Lean.ConstantInfo)

All user defined declarations.

Equations

• Physlib.allUserConsts = do let imports ← liftM Physlib.allImports let __do_lift ← Array.flatMapM Physlib.Imports.getUserConsts imports pure __do_lift