Porting wiki
Jeremy Tan Jie Rui edited this page 2023-07-16 10:11:32 +08:00

Page revisions

73 Commits

Author SHA1 Message Date
thorimur
52de0b4783 string shortening 2022-12-17 16:25:22 -05:00
Ruben Van de Velde
4011ae2f6d Updated Porting wiki (markdown) 2022-12-17 14:00:08 +01:00
Patrick Massot
273fb1345d Add Mathlib.lean updating command 2022-12-16 10:57:04 +01:00
Scott Morrison
bfe22c8cfe Updated Porting wiki (markdown) 2022-12-16 13:19:11 +11:00
thorimur
ba8da5f051 Updated Porting wiki (markdown) 2022-12-15 14:24:46 -05:00
thorimur
f109c4c6f1 clarify by adding rule about naming functions; remove `outParam` exception 2022-12-13 16:51:41 -05:00
Floris van Doorn
c4e7b1e482 Common fixes: use ↦ 2022-12-13 16:26:29 +01:00
Patrick Massot
48465795d0 Updated Porting wiki (markdown) 2022-12-13 15:57:22 +01:00
Frédéric Dupuis
e532cefa9b Add a link to Johan's port status page. 2022-12-11 19:20:23 -05:00
Heather Macbeth
5c86601615 Updated Porting wiki (markdown) 2022-12-09 14:59:42 +01:00
Heather Macbeth
83d1721c9c Updated Porting wiki (markdown) 2022-12-09 14:55:49 +01:00
Heather Macbeth
9b43b74788 Updated Porting wiki (markdown) 2022-12-08 14:21:06 +01:00
arienmalec
c96ea867bc Updated Porting wiki (markdown) 2022-12-07 22:30:05 -08:00
arienmalec
b1c612dc0d Updated Porting wiki (markdown) 2022-12-07 21:22:59 -08:00
Kevin Buzzard
e97a8e9f56 move autoImplicit hint 2022-12-03 13:56:04 +00:00
Kevin Buzzard
f68787eddc add autoImplicit hint 2022-12-03 13:54:54 +00:00
Kevin Buzzard
ba9294ec63 note that the video is slightly out of date. 2022-12-03 13:51:10 +00:00
Kevin Buzzard
c2309ccc1e remove claim that it's not clear what to do -- we know what to do now :-) 2022-12-03 13:50:30 +00:00
Kevin Buzzard
fc5202739a adding suggestions to minimise chances of duplicating work 2022-12-03 13:49:19 +00:00
Kevin Buzzard
ba6de65ff6 mention port progress bot 2022-12-03 13:44:16 +00:00
Eric Wieser
a4aa57a984 Formatting fix 2022-12-03 13:19:59 +00:00
Eric Wieser
3c127355fd Updated Porting wiki (markdown) 2022-12-03 13:04:54 +00:00
Frédéric Dupuis
786a106d9d I changed the page title from "Home" to something clearer. 2022-12-02 15:59:01 -05:00