From 3de7be028ad507db82abf757945ef39b57924c08 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 10 Apr 2026 14:12:30 +0200 Subject: [PATCH] fix: add type annotation to metadata In some very long documents with lots of subsections, this prevents an elaboration error on the metadata blocks. --- src/verso/Verso/Doc/Elab/Basic.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/verso/Verso/Doc/Elab/Basic.lean b/src/verso/Verso/Doc/Elab/Basic.lean index 4fe20620b..2044f4272 100644 --- a/src/verso/Verso/Doc/Elab/Basic.lean +++ b/src/verso/Verso/Doc/Elab/Basic.lean @@ -35,8 +35,9 @@ public partial def FinishedPart.toSyntax [Monad m] [MonadQuotation m] let subStx ← subParts.mapM (toSyntax genre) let metaStx ← match metadata with - | none => `(none) - | some stx => `(some $stx) + | none => ``(none) + | some stx => ``(some $stx) + let metaStx ← ``(($metaStx : Option (Verso.Doc.Genre.PartMetadata $genre))) -- Adding type annotations works around a limitation in list and array elaboration, where intermediate -- let bindings introduced by "chunking" the elaboration may fail to infer types let typedBlocks ← blocks.mapM fun b => `(($b : Block $genre))