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 racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
