зеркало из https://github.com/microsoft/ivy.git
23 строки
228 B
Plaintext
23 строки
228 B
Plaintext
|
#lang ivy1.7
|
||
|
|
|
||
|
|
# include order
|
||
|
|
|
||
|
|
type foo
|
||
|
|
interpret foo -> bv[3]
|
||
|
|
|
||
|
|
|
||
|
|
parameter max : foo = 3
|
||
|
|
|
||
|
|
action a (s:foo) returns (r:foo) = {
|
||
|
|
require s < max;
|
||
|
|
r := s + 1
|
||
|
|
}
|
||
|
|
|
||
|
|
action b returns (r:foo) = {
|
||
|
|
r := 0
|
||
|
|
}
|
||
|
|
|
||
|
|
export a
|
||
|
|
export b
|
||
|
|
|