polystlc 3
This commit is contained in:
parent
3b778e5db1
commit
63786c16b5
|
@ -6,3 +6,8 @@
|
||||||
< [(typeof Γ M (σ → σ_2))
|
< [(typeof Γ M (σ → σ_2))
|
||||||
---
|
---
|
||||||
> [(typeof Γ M (σ_2 → σ))
|
> [(typeof Γ M (σ_2 → σ))
|
||||||
|
294a295,298
|
||||||
|
> (define small-counter-example
|
||||||
|
> (term ((λ (x int) [nil @ int])
|
||||||
|
> [nil @ int])))
|
||||||
|
> (test-equal (check small-counter-example) #f)
|
||||||
|
|
|
@ -292,3 +292,7 @@
|
||||||
(generate-term poly-stlc M #:i-th index)
|
(generate-term poly-stlc M #:i-th index)
|
||||||
(set! index (add1 index))))))
|
(set! index (add1 index))))))
|
||||||
|
|
||||||
|
(define small-counter-example
|
||||||
|
(term ((λ (x int) [nil @ int])
|
||||||
|
[nil @ int])))
|
||||||
|
(test-equal (check small-counter-example) #f)
|
||||||
|
|
Loading…
Reference in New Issue
Block a user