The copyright linter

This file implements a linter that checks that every file in the project has the correct copyright header.

def CopyrightLinter.correctCopyrightPrefix : String

The part of the expected copyright before the year.

Equations

• CopyrightLinter.correctCopyrightPrefix = "/-\nCopyright "

def CopyrightLinter.correctCopyrightSuffix : String

The part of the expected copyright after the year.

Equations

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

def CopyrightLinter.hasCorrectCopyright (file : String) : Bool

Check whether a file, given as a String, is prefixed with the correct copyright header.

Equations

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

def CopyrightLinter.correctCopyrightHeader : String

The current correct copyright header.

Equations

• CopyrightLinter.correctCopyrightHeader = CopyrightLinter.correctCopyrightPrefix ++ "2026" ++ CopyrightLinter.correctCopyrightSuffix

opaque CopyrightLinter.linter.style.copyright : Lean.Option Bool

def CopyrightLinter.copyrightLinter : Lean.Linter

The copyright linter ensures that every file has the right copyright header.

Equations

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