Home

Reid Barton edited this page 2022-12-19 13:15:58 +01:00

Page revisions

69 Commits

Author	SHA1	Message	Date
Reid Barton	7919133955	Initial Home page	2022-12-19 13:15:58 +01:00
Frédéric Dupuis	786a106d9d	I changed the page title from "Home" to something clearer.	2022-12-02 15:59:01 -05:00
Ruben Van de Velde	176440af99	Updated Home (markdown)	2022-11-28 16:13:20 +01:00
arienmalec	39694557a7	Updated Home (markdown)	2022-11-27 21:20:34 -08:00
Winston Yin	312df13150	Updated Home (markdown)	2022-11-26 17:30:26 -08:00
Ruben Van de Velde	9a88a21507	Updated Home (markdown)	2022-11-26 15:30:09 +01:00
Winston Yin	5a0659bcf1	Updated Home (markdown)	2022-11-25 19:12:19 -08:00
Yury G. Kudryashov	a4974e7a68	Updated Home (markdown)	2022-11-25 00:42:38 -06:00
Floris van Doorn	6e12bd7b4d	remove outdated comment (since yesterday)	2022-11-24 19:05:42 +01:00
Floris van Doorn	f7713c88e8	Updated Home (markdown)	2022-11-24 18:17:50 +01:00
Floris van Doorn	80e77770fd	Updated Home (markdown)	2022-11-24 18:04:27 +01:00
Floris van Doorn	4cef87f7e1	update to_additive issues	2022-11-24 18:02:17 +01:00
Winston Yin	a0569176ba	Updated Home (markdown)	2022-11-23 23:15:38 -08:00
Winston Yin	26bcbe3037	Updated Home (markdown)	2022-11-23 23:13:37 -08:00
Winston Yin	c1594771a7	Updated Home (markdown)	2022-11-23 23:11:08 -08:00
Winston Yin	85278dc364	typo	2022-11-23 22:50:13 -08:00
Winston Yin	a5b3fc94c9	examples for naming convention	2022-11-23 22:49:24 -08:00
Winston Yin	8fba90c9c2	clarify	2022-11-23 22:16:54 -08:00
Winston Yin	fe33df73fd	update naming rules	2022-11-23 22:12:05 -08:00
arienmalec	1b213f622a	Updated Home (markdown)	2022-11-23 21:26:09 -08:00
Winston Yin	2ad892cc5f	fixed in #678	2022-11-23 18:57:52 -08:00
Eric Wieser	ca531a69ad	Remove instruction to run `add_port_comments`	2022-11-23 18:23:15 +00:00
Winston Yin	3e734b0a8e	typo	2022-11-22 17:48:33 -08:00
Winston Yin	917a8bee62	Updated Home (markdown)	2022-11-22 17:47:52 -08:00
Winston Yin	cdd1a9b6ca	Note on `to_additive`	2022-11-22 17:43:12 -08:00
Riccardo Brasca	576abbf454	Updated Home (markdown)	2022-11-21 15:19:18 +01:00
arienmalec	e16db58e73	Updated Home (markdown)	2022-11-20 08:47:23 -08:00
arienmalec	ca49cff1bc	Updated Home (markdown)	2022-11-20 08:46:48 -08:00
arienmalec	3ad547094b	Updated Home (markdown)	2022-11-20 08:16:42 -08:00
Eric Rodriguez	bca4349f10	SpecialNames is now Rename (I think?)	2022-11-20 11:00:40 -05:00
Moritz Doll	42ca08d58d	Explicit use of `coe`	2022-11-20 10:08:11 +01:00
Moritz Doll	95d7e8db5c	removed a single 'For'	2022-11-20 06:12:20 +01:00
arienmalec	c7ab27567a	Updated Home (markdown)	2022-11-19 20:14:44 -08:00
Eric Rodriguez	2db16eebb8	First commit should be the synported .lean	2022-11-19 18:55:43 -05:00
Eric Wieser	325acd3e81	Remove instructions about manual comments.	2022-11-19 11:14:09 +00:00
Moritz Doll	e6e0dace6e	Updated Home (markdown)	2022-11-19 03:34:55 +01:00
Moritz Doll	52bf49cd61	Updated Home (markdown)	2022-11-19 03:28:59 +01:00
Moritz Doll	c07cc86bf1	Updated Home (markdown)	2022-11-19 03:14:48 +01:00
Moritz Doll	edd66b008a	Updated Home (markdown)	2022-11-19 03:03:09 +01:00
Moritz Doll	a70d1bc285	Updated Home (markdown)	2022-11-19 02:55:15 +01:00
Moritz Doll	77e28ba0b3	Updated Home (markdown)	2022-11-19 02:54:25 +01:00
Moritz Doll	eee55a1b5d	Updated Home (markdown)	2022-11-19 02:52:01 +01:00
Moritz Doll	1a48ca7863	Updated Home (markdown)	2022-11-19 02:51:15 +01:00
Moritz Doll	de3ceddbbf	Updated Home (markdown)	2022-11-19 02:50:17 +01:00
Riccardo Brasca	7af03cd44b	Updated Home (markdown)	2022-11-18 13:32:16 +01:00
Riccardo Brasca	3eaa9dd0b1	Updated Home (markdown)	2022-11-18 12:22:43 +01:00
Riccardo Brasca	1d4db05def	Updated Home (markdown)	2022-11-18 11:11:15 +01:00
Jireh Loreaux	c5023d0cf4	Add instructions for finding and adding mathlib3 SHAs to appropriate places	2022-11-17 15:58:10 -06:00
Mario Carneiro	8a314e0117	Updated Home (markdown)	2022-11-17 12:55:25 -08:00
Mario Carneiro	ce09c3c48f	Updated Home (markdown)	2022-11-17 12:54:16 -08:00