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

2020-06-30 Thread Adrian Manea
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

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

2020-03-16 Thread Adrian Manea
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

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

2020-03-15 Thread Adrian Manea
mbda 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 details! What you'

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

2020-03-15 Thread Adrian Manea
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 AM Adrian Manea >

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

2020-03-15 Thread Adrian Manea
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 be other things that were glossed in the article? I don't know.) > > Cheers, > Matt > &

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

2020-03-15 Thread Adrian Manea
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