Regula rule reference

This page documents Regula 0.11.0. The latest release is Regula 0.11.1: this page in Regula 0.11.1.

Versions๐Ÿ”—

Regula
0.11.0
Commit
f85fcc138801de2154085b8e3f61fb42f5f25560
Lean toolchain (linter and examples)
4.34.1
Verso revision
cad4b633e75ea769b851f12f9ca3b4f0dfcc625f
Releases
0.11.0 for Lean 4.34.1, 0.10.0 for Lean 4.34.1, 0.9.0 for Lean 4.34.1, 0.8.0 for Lean 4.34.0, 0.7.0 for Lean 4.34.0, 0.6.0 for Lean 4.34.0, 0.5.0 for Lean 4.34.0, 0.4.3 for Lean 4.34.0, 0.4.2 for Lean 4.34.0, 0.4.1 for Lean 4.34.0, 0.4.0 for Lean 4.34.0, 0.3.1 for Lean 4.34.0, 0.3.0 for Lean 4.34.0, 0.2.0 for Lean 4.34.0, 4.34.0 for Lean 4.34.0
  • https://rbeauchamp.github.io/regula/ opens the latest release's copy, or the development version while no release exists: the stable address to share.

  • https://rbeauchamp.github.io/regula/dev/ is the development version, rebuilt from main by every deployment. An unreleased Regula build's findings link here.

  • https://rbeauchamp.github.io/regula/v/<version>/ is the permanent copy of a release, made when it is released. A released Regula build's findings link to its own release's copy. Once a later release exists, every page of an earlier copy names the latest release and links the same page there.

  • An address below https://rbeauchamp.github.io/regula/rules/ or https://rbeauchamp.github.io/regula/standard/ is a stable address. It names no version and opens the same page of the version that https://rbeauchamp.github.io/regula/ opens. It does not keep a fragment.

An address that names a version never redirects and never changes its meaning: dev/ is always the development version, and v/<version>/ is always the copy of that release. While a release exists, a stable address opens the same page of the latest release: its target moves at each release, and it has no page for a rule that no release has. To cite a rule as one release has it, use the address of that release.

A route that is not published shows the site's not-available page, which never redirects to other rules. Rule IDs are never reused for a changed rule; a retired rule keeps a page that says so.