Is there any way to generate a “fresh identifier” in a typing judgment in redex?

I see “fresh” but it appears to be a special form in a reduction relation.

escape to racket then gensym

Racket doesn’t really have support for lightweight slices does it? I can only copy a portion of a vector, byte-string, string, etc. I can’t just create a new object with an offset + length into an existing one to save memory?

escape to racket, yes, but gensym no — use variable-not-in or variables-not-in

This seems like a bug in string-split: (string-split "::XY" ":") ; => '("" "XY") I expected the output to be '("" "" "XY")

Racket v8.1.0.6 [cs]

Same output in 8.2 [cs]

Both of the following work as expected: (regexp-split #px":" "::XY") (string-split "::XY" ":" #:trim? #f) Ah… I misunderstood #:trim? - I assumed it was trimming whitespace. Sorry for the noise everyone !!!

I’m not sure #t is the best default for #trim?

@badkins Yes, easy to miss the trim part.

I just discovered hs-toggle-hiding which is provided by hideshow.el which Racket mode includes in Emacs. It’s very handy for collapsing large blocks of code that you don’t need to see. Rather than use both hs-hide-block and hs-show-block, using the single hs-toggle-hiding saves from using up more key chord space. I had C-c h available, so (global-set-key (kbd "C-c h") 'hs-toggle-hiding) in my Emacs config did the trick.

IIRC @notjack had done some thinking about views, and @hazel was doing some stuff with data processing. Not sure if they can help. I’m not aware of anything in core racket but i’m pretty new to the stdlib.

In TR is the difference between cast and assert that cast uses contracts vs assert using a predicate?

yes

Core racket doesn’t have support in the stdlib. We’d need generic collection interfaces. It’s something being considered for Rhombus though.