[racket-users] Re: Understanding P. Ragde's Proust

Thank you very much for coming back and posting this resource! I will be reading it carefully and I'm already sure there is a lot of useful content! Much appreciated. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this gro

[racket-users] Re: Understanding P. Ragde's Proust

Dear Prof. Ragde, Thank you very much for the reply! I watched your talk at the Racket con more carefully today and noticed you specifically point out that you don't give your students the whole code and that the entire project is presented as a "proof of concept" and used especially for didact

Re: [racket-users] Understanding P. Ragde's Proust

ck-proof > `((lambda x => x) : (A -> A))) > > this does not: > > (check-proof `((x : A) : A)) > > Hope that helps, > Matt > > > > On Sun, Mar 15, 2020 at 10:21 AM Adrian Manea > wrote: > >> Hi Matt, >> >> Thank you very much for the de

Re: [racket-users] Understanding P. Ragde's Proust

nday, March 15, 2020 at 2:32:42 PM UTC, Sorawee Porncharoenwase wrote: > > You need to add a case in parse-expr to deal with annotations, which is > in the form ( : ). > > E.g., > > [`(,e : ,t) (TA (parse-expr e) (parse-type t))] > > > On Sun, Mar 15, 2020 at 7:21 A

Re: [racket-users] Understanding P. Ragde's Proust

code as-is in a Github Gist > or similar, so that others can look at exactly what you're working with > would be useful. > > (I have no idea how complete or incomplete the code in the article is, > which is why I suggest you put it in a pastebin/gist to share... there > might

[racket-users] Understanding P. Ragde's Proust

Hi all, 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 "nano proof assistant" and work through the examples in his article. However, I'm pret