зеркало из https://github.com/microsoft/ivy.git
20 строки
181 B
Plaintext
20 строки
181 B
Plaintext
|
#lang ivy1.6
|
||
|
|
|
||
|
|
type t
|
||
|
|
|
||
|
|
relation p(X:t)
|
||
|
|
init p(X) <-> X = 1
|
||
|
|
|
||
|
|
action foo = {
|
||
|
|
if some x:t. p(x) {
|
||
|
|
call bar(x)
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|
||
|
|
action bar(x:t)
|
||
|
|
|
||
|
|
interpret t -> bv[1]
|
||
|
|
|
||
|
|
export foo
|
||
|
|
import bar
|