Typeclasses#46
Conversation
| Maps could go here as an example to reinforce this? Or maybe that's too long of an aside? The code | ||
| exists (with limited prose) in `Maps.lean` already. --CGH |
There was a problem hiding this comment.
I think the idea is to fold Maps into this chapter entirely, using it as an extended example to motivate typeclasses.
There was a problem hiding this comment.
I would be in support of this, I'll wait a bit to see that others agree before doing so.
There was a problem hiding this comment.
That was my impression also.
Co-authored-by: Daniel Sainati <sainatidaniel@gmail.com>
rogerburtonpatel
left a comment
rogerburtonpatel
left a comment
There was a problem hiding this comment.
Looks like a great start. I recommend a few more exercises, and some shifting of text, but it's already in a nice spot if we assume a post-indprop audience.
|
Note to self: confirmed in another PR that we will have structures by this point, so should use that in the initial explanation. |
|
I've had a quick look at the PR -- will review the chapter more thoroughly later, but I suggest we close the discussions on the PR, merge it, and continue thinking about all the remaining stuff at leisure. Doesn't seem to compile right now, though... |
I think there's something odd happening with the generated Lean files, I'll have a look. |
|
This wasn't building because the |
|
Build on this remains broken for two reasons, as best I can tell:
|
6 participants
This is a first pass at a chapter on typeclasses. This is still in a rough draft state, but I'm trying to follow Benjamin's request to PR things earlier if possible. There are a couple of organizational questions in my mind:
LF/Maps.leanI have already ported a version of that chapter, but using typeclasses. I left a placeholder here where it seems natural to fit in, but I wasn't sure if this was too long.LogicandIndProp. I left things unfinished towards the end where I wasn't sure what was important to translate.