That may be doable, based on what Burke is already working on. I think we've discussed it a little bit. (But probably not soon, I'm sorry to say.)
Robby On Tue, Aug 14, 2012 at 11:13 AM, Asumu Takikawa <as...@ccs.neu.edu> wrote: > On 2012-08-14 10:58:57 -0500, Robby Findler wrote: >> > Γ ⊦ ctc : (con t_1) >> > ----------------------------------------------- TConPrompt >> > Γ ⊦ (prompt/c t_2 ctc) : (con (prompt t_1 t_2)) >> > >> > and so on. Especially when you have multiple rules which induce these >> > extra type arguments. Maybe this is the best option though. >> >> t_2 here is the type of the result of the prompt expression? > > Yes, exactly, since the contract doesn't care what that is. > >> What would be the alternative construct? I guess define-judgment-form >> could switch into some kind of a prolog mode if there were no #:mode >> spec. And maybe that would be good enough for your model, generally >> speaking? > > That would be a nice addition, I think. It might not be pragmatic for > large models intended to closely model a real implementation, but for a > calculus (like the one I'm working on) I suspect it'd be performant > enough. > > Cheers, > Asumu ____________________ Racket Users list: http://lists.racket-lang.org/users
