chore: bump Lean toolchain

leanprover · Jan 3, 2024 · 0ff2297 · 0ff2297
1 parent 4e70b19
commit 0ff2297
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-12-04
+leanprover/lean4:nightly-2023-12-31
diff --git a/src/leandoc/LeanDoc/Doc/Concrete.lean b/src/leandoc/LeanDoc/Doc/Concrete.lean
@@ -59,10 +59,10 @@ elab "inlines!" s:inlineStr : term => open Lean Elab Term in
 set_option pp.rawOnError true
 
 /--
-info: #[Inline.text "Hello, ", Inline.emph #[Inline.bold #[Inline.text "emph"]]] : Array (Inline ?m.11031)
+info: #[Inline.text "Hello, ", Inline.emph #[Inline.bold #[Inline.text "emph"]]] : Array (Inline Genre.none)
 -/
 #guard_msgs in
-#check inlines!"Hello, _*emph*_"
+#check (inlines!"Hello, _*emph*_" : Array (Inline .none))
 
 def document : Parser where
   fn := rawFn <| atomicFn <| LeanDoc.Parser.document (blockContext := {maxDirective := some 6})
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:nightly-2023-12-04
		leanprover/lean4:nightly-2023-12-31