editing community extras

Stream: general

[Kevin Buzzard]

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]

It's this file right?

https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/templates/extras/simp.md

[Kevin Buzzard]

Looks good doesn't it. Thanks!

[Kevin Buzzard]

(I am having a serious case of structured procrastination)

[Bryan Gin-ge Chen]

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

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]

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