Normalise.

leanprover-community · Nov 2, 2024 · f4e4213 · f4e4213
1 parent 8b08db2
commit f4e4213
Showing 1 changed file with 42 additions and 35 deletions.
diff --git a/lean.bib b/lean.bib
@@ -777,23 +777,27 @@ @Article{         DupuisLewisMacbeth22
   tags          = {formalization, lean3}
 }
 
-@InProceedings{dvorak_et_al:LIPIcs.ITP.2023.15,
-  author =	{Dvorak, Martin and Blanchette, Jasmin},
-  title =	{{Closure Properties of General Grammars – Formally Verified}},
-  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
-  pages =	{15:1--15:16},
-  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
-  ISBN =	{978-3-95977-284-6},
-  ISSN =	{1868-8969},
-  year =	{2023},
-  volume =	{268},
-  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
-  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
-  address =	{Dagstuhl, Germany},
-  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.15},
-  URN =		{urn:nbn:de:0030-drops-183906},
-  doi =		{10.4230/LIPIcs.ITP.2023.15},
-  annote =	{Keywords: Lean, type-0 grammars, recursively enumerable languages, Kleene star},
+@InProceedings{   dvorak_et_al:LIPIcs.ITP.2023.15,
+  author        = {Dvorak, Martin and Blanchette, Jasmin},
+  title         = {{Closure Properties of General Grammars – Formally
+                  Verified}},
+  booktitle     = {14th International Conference on Interactive Theorem
+                  Proving (ITP 2023)},
+  pages         = {15:1--15:16},
+  series        = {Leibniz International Proceedings in Informatics
+                  (LIPIcs)},
+  isbn          = {978-3-95977-284-6},
+  issn          = {1868-8969},
+  year          = {2023},
+  volume        = {268},
+  editor        = {Naumowicz, Adam and Thiemann, Ren\'{e}},
+  publisher     = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
+  address       = {Dagstuhl, Germany},
+  url           = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.15},
+  urn           = {urn:nbn:de:0030-drops-183906},
+  doi           = {10.4230/LIPIcs.ITP.2023.15},
+  annote        = {Keywords: Lean, type-0 grammars, recursively enumerable
+                  languages, Kleene star},
   tags          = {formalization, lean3}
 }
 
@@ -1813,22 +1817,25 @@ @InProceedings{   YingDegenne23
   tags          = {formalization, lean3}
 }
 
-@InProceedings{Zhang23,
-  author =	{Zhang, Jujian},
-  title =	{{Formalising the Proj Construction in Lean}},
-  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
-  pages =	{35:1--35:17},
-  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
-  ISBN =	{978-3-95977-284-6},
-  ISSN =	{1868-8969},
-  year =	{2023},
-  volume =	{268},
-  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
-  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
-  address =	{Dagstuhl, Germany},
-  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.35},
-  URN =		{urn:nbn:de:0030-drops-184105},
-  doi =		{10.4230/LIPIcs.ITP.2023.35},
-  annote =	{Keywords: Lean, formalisation, algebraic geometry, scheme, Proj construction, projective geometry},
+@InProceedings{   Zhang23,
+  author        = {Zhang, Jujian},
+  title         = {{Formalising the Proj Construction in Lean}},
+  booktitle     = {14th International Conference on Interactive Theorem
+                  Proving (ITP 2023)},
+  pages         = {35:1--35:17},
+  series        = {Leibniz International Proceedings in Informatics
+                  (LIPIcs)},
+  isbn          = {978-3-95977-284-6},
+  issn          = {1868-8969},
+  year          = {2023},
+  volume        = {268},
+  editor        = {Naumowicz, Adam and Thiemann, Ren\'{e}},
+  publisher     = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
+  address       = {Dagstuhl, Germany},
+  url           = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.35},
+  urn           = {urn:nbn:de:0030-drops-184105},
+  doi           = {10.4230/LIPIcs.ITP.2023.35},
+  annote        = {Keywords: Lean, formalisation, algebraic geometry, scheme,
+                  Proj construction, projective geometry},
   tags          = {formalization, lean3}
-}
+}