From bf31028b3abf18e940cf6bb0c9128acbd220a67f Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 5 Jul 2025 13:21:41 +0200 Subject: [PATCH] chore: avoid immediate jargon --- Manual/ModuleSystem.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/ModuleSystem.lean b/Manual/ModuleSystem.lean index af277953..73a4219f 100644 --- a/Manual/ModuleSystem.lean +++ b/Manual/ModuleSystem.lean @@ -15,7 +15,7 @@ open Verso.Genre.Manual.InlineLean number := false %%% -The module system is an experimental feature that allows for more fine-grained control over what information is exported from, and imported into, modules. +The module system is an experimental feature that allows for more fine-grained control over what information is exported from, and imported into, Lean files. The main benefits of doing so are: