Skip to content

Commit 0758b1d

Browse files
authored
doc: update parse function documentation (#14174)
This PR updates the docstrings for `Std.Time.GenericFormat.parse` and `Std.Time.GenericFormat.parse!` to say that they parse into `DateTime`, matching their return types. Codex (OpenAI's coding agent) was used to draft the PR description. Closes #14173
1 parent d29f6a4 commit 0758b1d

1 file changed

Lines changed: 2 additions & 2 deletions

File tree

src/Std/Time/Format/Basic.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1410,13 +1410,13 @@ def builderParser (format: FormatString) (config : FormatConfig) (func: FormatTy
14101410
go format func
14111411

14121412
/--
1413-
Parses the input string into a `ZoneDateTime`.
1413+
Parses the input string into a `DateTime`.
14141414
-/
14151415
def parse (format : GenericFormat aw) (input : String) : Except String DateTime :=
14161416
(parser format.string format.config aw <* eof).run input
14171417

14181418
/--
1419-
Parses the input string into a `ZoneDateTime` and panics if its wrong.
1419+
Parses the input string into a `DateTime` and panics if its wrong.
14201420
-/
14211421
def parse! (format : GenericFormat aw) (input : String) : DateTime :=
14221422
match parse format input with

0 commit comments

Comments
 (0)