[racket] Using Redex for type systems w/ unconstrained variables

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.

Thanks,
Asumu