Re: [racket-users] PLT Redex & dependent type

It is very helpful to me. You are so nice! Thank you very much! On Tuesday, April 10, 2018 at 9:35:31 PM UTC+8, William J. Bowman wrote: > > FYI, I have some other models here: > - A model of Luo's ECC, a much smaller model than CIC: > https://github.com/wilbowma/ecc-redex > - A couple of

Re: [racket-users] PLT Redex & dependent type

FYI, I have some other models here: - A model of Luo's ECC, a much smaller model than CIC: https://github.com/wilbowma/ecc-redex - A couple of experimental models, including a model with just Π, and failed attempt (IIRC) to model Hoare Type Theory: https://github.com/wilbowma/dep-types-101

Re: [racket-users] PLT Redex & dependent type

Yes. https://github.com/wilbowma/cic-redex This isn't exactly a minimal example; I have a smaller model somewhere I'll try to send. -- Sent from my phoneamajig > On Apr 10, 2018, at 06:32, Ning Shan wrote: > > Can I implement dependent type in PLT Redex? >

[racket-users] PLT Redex & dependent type

Can I implement dependent type in PLT Redex? https://en.wikipedia.org/wiki/Dependent_type Specifically Pi type. Can anyone give me a reference or a minimal example? Thanks in advance. :-) -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To