add existential tests demonstrating hidden type
This commit is contained in:
parent
33996e71ac
commit
dad2c26c49
|
@ -76,6 +76,14 @@
|
|||
(∃ (Counter) (× [new : Counter]
|
||||
[get : (→ Counter Int)]
|
||||
[inc : (→ Counter Counter)])))
|
||||
(typecheck-fail
|
||||
(open ([(Counter counter) <= counterADT])
|
||||
(+ (proj counter new) 1))
|
||||
#:with-msg "Arguments to function \\+ have wrong type")
|
||||
(typecheck-fail
|
||||
(open ([(Counter counter) <= counterADT])
|
||||
((λ ([x : Int]) x) (proj counter new)))
|
||||
#:with-msg "Arguments to function.+have wrong type")
|
||||
(check-type
|
||||
(open ([(Counter counter) <= counterADT])
|
||||
((proj counter get) ((proj counter inc) (proj counter new))))
|
||||
|
|
Loading…
Reference in New Issue
Block a user