Zulip Chat Archive

Stream: general

Topic: editing community extras


view this post on Zulip 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.

view this post on Zulip Shing Tak Lam (Jan 03 2021 at 10:55):

It's this file right?

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

view this post on Zulip Kevin Buzzard (Jan 03 2021 at 10:56):

Looks good doesn't it. Thanks!

view this post on Zulip Kevin Buzzard (Jan 03 2021 at 11:07):

(I am having a serious case of structured procrastination)

view this post on Zulip 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.)

view this post on Zulip 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 :) )

view this post on Zulip 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: May 18 2021 at 16:25 UTC