chotu·12년 전·discussIn ATS2 you can do like this :fun foo {n : int | n > 2} (x : int (n)) : void = println! (x)now calling foo (10) will type check but foo (2) or foo (1) will not.
chotu·12년 전·discussThere seem to be misconception that safe language implies inefficient and slow code . It is not so in ATS2 , generated code is quite efficient and is safe even when manipulating memory from ATS2 .
chotu·12년 전·discussYou can do specification as type in ATS2 too. My biased view is that I find ATS2 to be far more practical than using coq.
fun foo {n : int | n > 2} (x : int (n)) : void = println! (x)
now calling foo (10) will type check but foo (2) or foo (1) will not.