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 |
|