racket / redex

Other
93 stars 36 forks source link

`(in-hole E hole)` typesets as just `E` #210

Closed florence closed 4 years ago

florence commented 4 years ago

In the program:

#lang racket
(require redex/reduction-semantics
         redex/pict)
(define-language L
  (E ::= hole (add1 E)))
(render-term L (in-hole E hole))

I get back a pict containing just E, rather than E[[]], which I would expect.

https://github.com/samth/plt-history/commit/341d0c76a9bcacebcc959eb8982cf0b5d472f42c#diff-40d2b8fe4358be37c0192b0c40eda357R71

makes this seem like a deliberate choice. However I find myself needing wanting typeset E[[]]=E in an explanation, which I currently can't do.

rfindler commented 4 years ago

I think that was probably a bad choice on my part and am reluctantly okay with a backwards incompatible change here.

On Mon, Dec 2, 2019 at 3:14 PM Spencer Florence notifications@github.com wrote:

In the program:

lang racket

(require redex/reduction-semantics redex/pict) (define-language L (E ::= hole (add1 E))) (render-term L (in-hole E hole))

I get back a pict containing just E, rather than E[[]], which I would expect.

samth/plt-history@341d0c7#diff-40d2b8fe4358be37c0192b0c40eda357R71 https://github.com/samth/plt-history/commit/341d0c76a9bcacebcc959eb8982cf0b5d472f42c#diff-40d2b8fe4358be37c0192b0c40eda357R71

makes this seem like a deliberate choice. However I find myself needing wanting typeset E[[]]=E in an explanation, which I currently can't do.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/racket/redex/issues/210?email_source=notifications&email_token=AADBNMHNMXJO4ZOJYIHMCSLQWVUD3A5CNFSM4JUFUH32YY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4H5OHPYA, or unsubscribe https://github.com/notifications/unsubscribe-auth/AADBNMDRUM6CLLFTOXVEKVLQWVUD3ANCNFSM4JUFUH3Q .

rfindler commented 4 years ago

merged #211.