parent
4bfd6ff6e3
commit
b63aa6bbac
|
@ -21,7 +21,8 @@
|
||||||
racket/syntax
|
racket/syntax
|
||||||
syntax/id-table
|
syntax/id-table
|
||||||
racket/list
|
racket/list
|
||||||
syntax/parse))
|
syntax/parse
|
||||||
|
syntax/stx))
|
||||||
|
|
||||||
(require
|
(require
|
||||||
(for-template "term.rkt"))
|
(for-template "term.rkt"))
|
||||||
|
@ -720,9 +721,9 @@
|
||||||
(define-syntax (judgment-holds stx)
|
(define-syntax (judgment-holds stx)
|
||||||
(syntax-case stx ()
|
(syntax-case stx ()
|
||||||
[(_ (jf-id . args))
|
[(_ (jf-id . args))
|
||||||
#'(#%expression (judgment-holds/derivation judgment-holds #f (jf-id . args)))]
|
#`(#%expression (judgment-holds/derivation judgment-holds #f #,(stx-car (stx-cdr stx))))]
|
||||||
[(_ (jf-id . args) trm)
|
[(_ (jf-id . args) trm)
|
||||||
#'(#%expression (judgment-holds/derivation judgment-holds #f (jf-id . args) trm))]))
|
#`(#%expression (judgment-holds/derivation judgment-holds #f #,(stx-car (stx-cdr stx)) trm))]))
|
||||||
|
|
||||||
(define-syntax (build-derivations stx)
|
(define-syntax (build-derivations stx)
|
||||||
(syntax-case stx ()
|
(syntax-case stx ()
|
||||||
|
|
|
@ -2,7 +2,7 @@
|
||||||
([not-judgment-form junk])
|
([not-judgment-form junk])
|
||||||
(judgment-holds (not-judgment-form z (s z))))
|
(judgment-holds (not-judgment-form z (s z))))
|
||||||
|
|
||||||
(#rx"a?: mode specifies a 1-ary relation but use supplied 2 terms"
|
(#rx"a[?]: mode specifies a 1-ary relation but use supplied 2 terms"
|
||||||
([bad-judgment (a? a q)])
|
([bad-judgment (a? a q)])
|
||||||
([name a?])
|
([name a?])
|
||||||
(let ()
|
(let ()
|
||||||
|
|
Loading…
Reference in New Issue
Block a user