On Tue, Aug 14, 2012 at 10:45 AM, Asumu Takikawa <as...@ccs.neu.edu> wrote: > On 2012-08-14 10:26:14 -0500, Robby Findler wrote: >> ----------------- >> Γ ⊦ (error t) : t > > That's what I meant. It's not so bad here, but it's more awkward in > other cases: > > Γ ⊦ ctc : (con t_1) > ------------------------------------------- TConPrompt > Γ ⊦ (prompt/c ctc) : (con (prompt t_1 t_2)) > > which has to look like > > Γ ⊦ 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? Yeah, I think that's the best option (but I like to see Redex being used....) 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? Robby ____________________ Racket Users list: http://lists.racket-lang.org/users
