From 664cc76f28a57a2d2431a8777e92658a0e8dcc6d Mon Sep 17 00:00:00 2001
From: Moritz Doll <moritz.doll@googlemail.com>
Date: Wed, 24 Jun 2026 17:25:13 +1000
Subject: [PATCH] print version in verso

---
 DynamicalSystems/Documentation.lean | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/DynamicalSystems/Documentation.lean b/DynamicalSystems/Documentation.lean
index 1c2961b..d4e266e 100644
--- a/DynamicalSystems/Documentation.lean
+++ b/DynamicalSystems/Documentation.lean
@@ -13,6 +13,13 @@ set_option linter.hashCommand false
 
 set_option pp.rawOnError true
 
+open Verso Doc Elab in
+@[role_expander leanVersion]
+def leanVersion : RoleExpander
+  | #[], #[] => do
+    return #[← ``(Verso.Doc.Inline.code $(Lean.Quote.quote Lean.versionString))]
+  | _, _ => throwError "Unexpected arguments"
+
 #doc (Manual) "Nonlinear dynamical systems & control theory" =>
 
 %%%
@@ -22,7 +29,8 @@ authors := ["Moritz Doll", "Iman Shames"]
 This repository develops the mathematical foundations of nonlinear dynamical systems and control
 theory.
 
-The code is hosted on [Github](https://github.com/mcdoll/DynamicalSystems).
+The code is hosted on [Github](https://github.com/mcdoll/DynamicalSystems) and compiled with
+Lean {leanVersion}[].
 
 {include 1 DynamicalSystems.Mathlib.Analysis.ODE.Documentation}
 {include 1 DynamicalSystems.Basic.Documentation}