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]> 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]. > 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.

