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 experimental models, including a model with just Π, and > failed attempt (IIRC) to model > Hoare Type Theory: https://github.com/wilbowma/dep-types-101 > > -- > William J. Bowman > > On Tue, Apr 10, 2018 at 07:53:37AM -0400, 'William J. Bowman' via Racket > Users wrote: > > 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 <[email protected] <javascript:>> > wrote: > > > > > > 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 unsubscribe from this group and stop receiving emails from it, send > an email to [email protected] <javascript:>. > > > For more options, visit https://groups.google.com/d/optout. > > > > -- > > 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] <javascript:>. > > For more options, visit https://groups.google.com/d/optout. >
-- 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]. For more options, visit https://groups.google.com/d/optout.
