Regula rule reference

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

Versions๐Ÿ”—

Regula
0.8.0
Commit
01362986ce7eea378ed3f0d81ca082150ff7c2ac
Lean toolchain (linter and examples)
4.34.0
Verso revision
cad4b633e75ea769b851f12f9ca3b4f0dfcc625f
Releases
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.

A route that is not published shows the site's not-available page. It never redirects to other rules: an old link cannot silently acquire changed semantics. Rule IDs are never reused for a changed rule; a retired rule keeps a page that says so.