Joachim Breitner 34264a4b1d doc: Improve docstrings around Array.mk,.data,.toList (#2771) ... following a discussion at <https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Understanding.20the.20docstring.20for.20docs.23Array.2Edata/near/398705430> --------- Co-authored-by: Mario Carneiro <di.gama@gmail.com>		2023-11-29 08:49:13 +00:00
..
Basic.lean	doc: Improve docstrings around Array.mk,.data,.toList (#2771)	2023-11-29 08:49:13 +00:00
BasicAux.lean	chore: snake-case attributes (part 2)	2022-10-19 09:28:08 -07:00
BinSearch.lean	chore: remove [Inhabited A] from binSearch / binInsert	2022-11-13 15:00:26 -08:00
DecidableEq.lean	refactor: prepare to elaborate a[i] notation using typeclasses	2022-07-09 15:24:22 -07:00
InsertionSort.lean	feat: use sepBy1Indent for tactic blocks	2022-09-18 16:43:23 -07:00
Mem.lean	doc: fix typo in Array.Mem docstring (#2856)	2023-11-10 11:16:32 +00:00
QSort.lean	fix: remove Inhabited Environment instance	2022-12-21 20:08:08 +01:00
Subarray.lean	fix: notation unexpander on overapplication of non-nullary notation	2023-01-26 13:05:33 +01:00