From 413a24da56490189334a76a71f87ebf5a45474b0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sun, 12 Dec 2021 13:18:24 +0100
Subject: [PATCH] feat: improve HTML to String a bit

---
 DocGen4/ToHtmlFormat.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/DocGen4/ToHtmlFormat.lean b/DocGen4/ToHtmlFormat.lean
index 2b617d2..b2f4629 100644
--- a/DocGen4/ToHtmlFormat.lean
+++ b/DocGen4/ToHtmlFormat.lean
@@ -33,7 +33,6 @@ def attributesToString (attrs : Array (String × String)) :String :=
 
 -- TODO: Termination proof
 partial def toStringAux : Html → String
-| element tag attrs #[] => s!"<{tag}{attributesToString attrs}/>\n"
 | element tag attrs #[text s] => s!"<{tag}{attributesToString attrs}>{s}</{tag}>\n"
 | element tag attrs #[child] => s!"<{tag}{attributesToString attrs}>\n{child.toStringAux}</{tag}>\n"
 | element tag attrs children => s!"<{tag}{attributesToString attrs}>\n{children.foldl (· ++ toStringAux ·) ""}</{tag}>\n"