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
