As far as I understand, your ‘length-ok’ is implementing in Redex the ‘(<= (length ___) ___)’ I had in my ‘side-condition’. But I can’t see how it addresses two important features from my original code: (1) ‘k’ is parameterizable, and its value influences whether a list is valid or not; and (2) the non-terminal ‘t’ could appear in patterns, for example, in a metafunction contract. This last one is essential, because using ‘t’ in a contract enforces a data structure invariant—‘t’ can’t be longer than ‘k’—and I can’t trust all callers of my metafunctions to check ‘length-ok’ themselves. In some cases, they wouldn’t even be able to do it; for example, suppose ‘t’ is part of the ‘domain’ of a ‘reduction-relation’ and I use it with ‘apply-reduction-relation*’, then there’s no way to access intermediary states and check if they preserve the invariant.
-- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. For more options, visit https://groups.google.com/d/optout.
