www

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

check-type+asserts.rkt (530B)

      1 #lang racket/base
      2 
      3 (provide check-type+asserts)
      4 
      5 (require turnstile/turnstile
      6          "check-asserts.rkt"
      7          (only-in "../../rosette/rosette2.rkt" CListof Bool CUnit))
      8 
      9 (define-typed-syntax check-type+asserts #:datum-literals (: ->)
     10   [(_ e : τ-expected -> v asserts) ≫
     11    [⊢ [e ≫ e- ⇐ : τ-expected]]
     12    --------
     13    [⊢ [_ ≫ (check-equal?/asserts e-
     14                                  (add-expected v τ-expected)
     15                                  (add-expected asserts (CListof Bool)))
     16          ⇒ : CUnit]]])
     17