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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/55610873-9554-4ce5-b5a6-33a7d29524bb%40googlegroups.com.
