Zulip Chat Archive

Stream: general

Topic: editing community extras

Kevin Buzzard (Jan 03 2021 at 10:50):

This page about simp drives me nuts. I wrote it when I didn't have a clue what was going on and what was important -- in fact it was born as notes to myself explaining to me what the simplifier did. But I don't know how to edit it. Is there some simp.md file somewhere in some github repo that I could make a PR to? I want to write somenthing which is more useful for both beginners and experts.

Shing Tak Lam (Jan 03 2021 at 10:55):

It's this file right?


Kevin Buzzard (Jan 03 2021 at 10:56):

Looks good doesn't it. Thanks!

Kevin Buzzard (Jan 03 2021 at 11:07):

(I am having a serious case of structured procrastination)

Bryan Gin-ge Chen (Jan 03 2021 at 16:04):

(For future reference, there's a link at the very bottom of the page that says "Suggest edits to this page on GitHub", which leads to the source file.)

Floris van Doorn (Jan 03 2021 at 22:39):

Kevin Buzzard said:

(I am having a serious case of structured procrastination)

That hits really close to home. Lean formalization is especially easy when I have something more important to do (like, finishing my slides for a presentation I have to give the next day :) )

Kevin Buzzard (Jan 03 2021 at 22:41):

It worked for me today -- I made a PR. I'd better do those references for all those poor students tomorrow morning though!

Last updated: Aug 03 2023 at 10:10 UTC