def DocGen4.Output.SourceLinker.mkGithubSourceLinker (baseUrl : String) (range : Option Lean.DeclarationRange) : String

Equations

• DocGen4.Output.SourceLinker.mkGithubSourceLinker baseUrl (some range_2) = toString baseUrl ++ toString "#L" ++ toString range_2.pos.line ++ toString "-L" ++ toString range_2.endPos.line
• DocGen4.Output.SourceLinker.mkGithubSourceLinker baseUrl none = baseUrl

def DocGen4.Output.SourceLinker.mkVscodeSourceLinker (baseUrl : String) (range : Option Lean.DeclarationRange) : String

Equations

• DocGen4.Output.SourceLinker.mkVscodeSourceLinker baseUrl (some range_2) = toString baseUrl ++ toString ":" ++ toString range_2.pos.line ++ toString ":" ++ toString (range_2.pos.column + 1)
• DocGen4.Output.SourceLinker.mkVscodeSourceLinker baseUrl none = baseUrl

def DocGen4.Output.SourceLinker.sourceLinker (gitUrl? : Option String) (module : Lean.Name) : Option Lean.DeclarationRange → String

Given a lake workspace with all the dependencies as well as the hash of the compiler release to work with this provides a function to turn names of declarations into (optionally positional) Github URLs.

Equations

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