add test case for new behavior (that I think was
legtimately a bug before the recent change to metafunction contracts that added #:post)
This commit is contained in:
parent
83a76027d5
commit
a984e828dd
|
@ -1185,6 +1185,15 @@
|
|||
'(2 1)))
|
||||
|
||||
(let ()
|
||||
|
||||
(define-metafunction empty-language
|
||||
must-be-identity : natural_1 -> natural_1
|
||||
[(must-be-identity any) 0])
|
||||
|
||||
(test (with-handlers ((exn:fail:redex? exn-message))
|
||||
(term (must-be-identity 1)))
|
||||
#rx"codomain test failed")
|
||||
|
||||
(define-metafunction empty-language
|
||||
[(same any_1 any_1) #t]
|
||||
[(same any_1 any_2) #f])
|
||||
|
|
Loading…
Reference in New Issue
Block a user