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 wrote:
> On 2012-08-14 10:58:57 -0500, Robby Findler wrote:
>> >Γ ⊦ ctc : (con t_1
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 argum
On Tue, Aug 14, 2012 at 10:45 AM, Asumu Takikawa 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)
> -
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
In addition to those options (or maybe this is what you meant by
option 3, but your words make it seem more drastic than it appears to
be, at least to me), you could go with what the literature does,
namely add more than one 'error', one for each type. Typeset it
something like "error" with a subsc
Hi all,
I've hit a problem with using Redex for designing type systems and
wanted to see if anyone had any ideas for working around it.
Background: Redex now offers the nice `define-judgment-form` feature for
defining things like type rules. These judgments can specify either I or
O (input or out
6 matches
Mail list logo
