From b4099230b94440afe0c2bbe933ed7adb2be1199c Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Thu, 4 Sep 2025 16:20:28 +0200 Subject: [PATCH 1/4] test --- Manual/Order/Test.lean | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 Manual/Order/Test.lean diff --git a/Manual/Order/Test.lean b/Manual/Order/Test.lean new file mode 100644 index 00000000..a5fd2c12 --- /dev/null +++ b/Manual/Order/Test.lean @@ -0,0 +1,23 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Paul Reichert +-/ + +import VersoManual + +import Manual.Meta + +open Manual.FFIDocType + +open Verso.Genre Manual +open Verso.Genre.Manual.InlineLean + +set_option pp.rawOnError true + +#doc (Manual) "Order typeclasses" => +%%% +tag := "order" +%%% + +Lorem ipsum From d52438ed24dfe71c1de33c3d90ca9c43f01e5d95 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Thu, 4 Sep 2025 16:24:45 +0200 Subject: [PATCH 2/4] import --- Manual.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Manual.lean b/Manual.lean index 3b8ae542..8e984bb9 100644 --- a/Manual.lean +++ b/Manual.lean @@ -29,6 +29,7 @@ import Manual.Releases import Manual.Namespaces import Manual.Runtime import Manual.ModuleSystem +import Manual.Order.Test open Verso.Genre Manual open Verso.Genre.Manual.InlineLean From b5123b562fc86a0eadded7639f5206853497666d Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Thu, 4 Sep 2025 16:34:07 +0200 Subject: [PATCH 3/4] ... --- Manual.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Manual.lean b/Manual.lean index 8e984bb9..ad0b7cb0 100644 --- a/Manual.lean +++ b/Manual.lean @@ -142,6 +142,8 @@ Overview of the standard library, including types from the prelude and those tha {include 0 Manual.Releases} +{include 0 Manual.Order.Test} + # Index %%% number := false From 56fb7bbc07ea798718099bd666c0ac5e5324c683 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Fri, 5 Sep 2025 15:23:46 +0200 Subject: [PATCH 4/4] iterators --- Manual/Order/Test.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Manual/Order/Test.lean b/Manual/Order/Test.lean index a5fd2c12..604f494b 100644 --- a/Manual/Order/Test.lean +++ b/Manual/Order/Test.lean @@ -15,9 +15,9 @@ open Verso.Genre.Manual.InlineLean set_option pp.rawOnError true -#doc (Manual) "Order typeclasses" => +#doc (Manual) "Iterators and Ranges" => %%% -tag := "order" +tag := "iterators" %%% Lorem ipsum