On Sunday, March 15, 2020 at 10:00:59 AM UTC-4, Adrian Manea wrote: > > > I'm a mathematician delving into type theory and proof assistants and with > special interests in Racket. > > I'm now trying to understand and implement P. Ragde's Proust > <https://arxiv.org/abs/1611.09473> "nano proof assistant" and work > through the examples in his article. However, I'm pretty much a beginner in > Racket and I'm getting some errors. >
Hi! Sorry, I only get this list as a digest, so I didn't see your message until this morning. The code in the paper is not complete, and the paper isn't written so that a beginner in Racket could easily extract a working program from it. When I teach students this material, I give them a working starter file, and I will send that to you by private email, where we can also continue to discuss as needed. I am at this moment working on converting my course materials on this topic into a free online resource similar to the one I did for functional data structures. But this is not ready yet. I hope to finish it in the next few months and I will post here when it is ready. --PR -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/55610873-9554-4ce5-b5a6-33a7d29524bb%40googlegroups.com.
