Support for infix dots

[wilbowma]

trafficstars

I want to write an infix expression but I can't use {} to make it infix, but neither can I use infix dots:

define-syntax ⊢
 syntax-rules (:)
   [(⊢ Γ e : t) (void)]

;; I didn't expect this would work
{Γ ⊢ e2 : t}

;; but this doesn't work either
(Γ . ⊢ . e2 : t)

[AlexKnauth]

Infix dots would be a good thing to support. I've also wanted to use them for -> contracts.

But for your case, if you define an nfx macro, you can have it recognize ⊢ and transform it:

#lang sweet-exp racket

define-syntax ⊢
  syntax-rules (:)
    [(⊢ Γ e : t) (void)]

define-syntax nfx
  syntax-rules (⊢ :)
    [(nfx Γ ⊢ e : t)
     (⊢ Γ e : t)]

{Γ ⊢ e2 : t}

[wilbowma]

Oh. Hm. That seems awkward and non-local, but I suppose that works.