-
Notifications
You must be signed in to change notification settings - Fork 34
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
WIP Smallstep + Types + STLC + StlcProp #50
base: develop
Are you sure you want to change the base?
Conversation
Hey, thanks for the help! I'll try to review in the next few days. |
I see you have added the |
Hi Alex, Here some remarks: Namespaces: (This caused me problems as well when doing the first chapter exercises, which I couldn't resolve Syntax: Big versus Small letters: Implicit aruments: Proofs: Documentation generation: In the Makefile PANDOC_FLAGS As well I would like to add --strip-comments to the PANDOC_FLAGS, because this gives the opportunity to As well I had to take out this two lines from book.tex to make it work:
Can I check the changes in my pull request, or should I do a seperate pull request? As well sillyfun1_odd from Tactics is not working for minted, and latex can't recover from this. I found some problems with prooftrees in Imp.lidr. Can I check in the current pdf in my pull request to become already useful for interested learners? Suggestion: Best regards |
Thanks for this. I’ll try to check it out sometime between tonight and Monday. |
So, just to let you know, I've started reviewing |
That fits well, as I start with one more chapter. |
@jutaro I've pushed my WIP post-review fixes for |
I scanned your changes, and see that I made some errors with exercises and that the complicated proofs now looks much nicer! I have one problem when compiling, and get the following error, which I don't understand. But I have idris 1.3.0, so maybe I shall upgrade to 1.3.1? Smallstep.lidr:278:3-65: |
Oops, pushed an update. |
Now it compiles, you are working on the imperative part. Cool |
Ok I think I'm done with |
This pull request is just to make you aware that I try to port the Smallstep chapter. Help welcome and needed.