From f7307953d84be8b1edaff97436e67434111244b0 Mon Sep 17 00:00:00 2001
From: Henrik <hargonix@gmail.com>
Date: Sun, 10 Sep 2023 14:44:14 +0200
Subject: [PATCH] fix: sort expression printing

---
 DocGen4/Output/Base.lean | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
index e2ae134..8fab52a 100644
--- a/DocGen4/Output/Base.lean
+++ b/DocGen4/Output/Base.lean
@@ -254,11 +254,12 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
       | .sort _ =>
         match t with
         | .text t =>
-          let mut sortPrefix :: rest := t.splitOn " " | unreachable!
+          let sortPrefix :: rest := t.splitOn " " | unreachable!
           let sortLink := <a href={s!"{← getRoot}foundational_types.html"}>{sortPrefix}</a>
-          if rest != [] then
-            rest := " " :: rest
-          return #[sortLink, Html.text <| String.join rest]
+          let mut restStr := String.intercalate " " rest
+          if restStr.length != 0 then
+            restStr := " " ++ restStr
+          return #[sortLink, Html.text restStr]
         | _ =>
           return #[<a href={s!"{← getRoot}foundational_types.html"}>[← infoFormatToHtml t]</a>]
       | _ =>