redex
redex copied to clipboard
racket
```racket #lang racket (require redex) (define-language A (N ::= 0 1 2)) (define-metafunction A flip : N -> N [(flip 1) ()] [(flip ()) 1]) (term (flip 1)) ; flip:...
**What version of Racket are you using?** e.g., 8.4 [cs] **What program did you run?** I'm experimenting with redex; perhaps this is known behavior. I found it surprising that parts...
Consider the following program: ```racket #lang racket/base (require redex/reduction-semantics) (define-language L (self ::= (self))) (define-judgment-form L #:mode (--> I O) #:contract (--> self self) [----------- "Do Nothing" (--> (self) (self))])...
I noticed in the redex reference that the default #:steps value is 1000. However, would it be useful if this specific case maybe fails since the reduction require much smaller...
I can't reproduce this reliably with all terms but, observe the far right term: It's cut off for some reason. But if I *narrow* the box, then it display correctly....
I was trying to specify a language that has a sort of rudimentary module system. The idea is that a module consists of 0 or more imports (which are themselves...
make it easy to rewrite other atoms in redex models (e.g. a language might want to use `#t` and `#f` because it is convenient, but render them as `true` and...
_Original text by @rfindler_. In general, this aspect of the handling of ellipses is implemented by the `racket/datum` library (the same library that `syntax-case` uses). It can cope with writing...
I don't even know what to make of this. ```racket #lang racket (require redex/reduction-semantics) (define-language Boxy (e ::= x (λ (x : t) e) (e e)) (t ::= nat (→...
I usually think of any term being allowed in pattern position and simply acting as "unify with this". I think of define-term as simply introducing a meta-variable that means literally...