lean-liquid icon indicating copy to clipboard operation
lean-liquid copied to clipboard
verified publisher icon leanprover-community

add more comments

Open kbuzzard opened this issue 3 years ago • 1 comments

This PR does a couple of things.

  1. I remove all irrelevant imports, opens and open-locales. Undocumented and unused commands just confuse the non-expert reader.

  2. I write the document the way I write my teaching documents; every single thing which is left I attempt to explain.

kbuzzard avatar Aug 27 '22 15:08 kbuzzard

One reason why we had the irrelevant imports and open_locales is because that proves (or at least makes it very likely) that we didn't do weird abuses of notation.

jcommelin avatar Aug 31 '22 06:08 jcommelin