www

Unnamed repository; edit this file 'description' to name the repository.
Log | Files | Refs | README

render.rkt (457B)

      1 #lang turnstile
      2 (require
      3  (prefix-in t/ro: (only-in "../rosette2.rkt" CNat CSolution CPict))
      4  (prefix-in ro: rosette/lib/render))
      5 (provide render)
      6 
      7 (define-typed-syntax render
      8   [(_ s) ≫
      9    [⊢ [s ≫ s- ⇐ : t/ro:CSolution]]
     10    --------
     11    [⊢ [_ ≫ (ro:render s-) ⇒ : t/ro:CPict]]]
     12   [(_ s sz) ≫
     13    [⊢ [s ≫ s- ⇐ : t/ro:CSolution]]
     14    [⊢ [sz ≫ sz- ⇐ : t/ro:CNat]]
     15    --------
     16    [⊢ [_ ≫ (ro:render s- sz-) ⇒ : t/ro:CPict]]])
     17