ivy/test/annot1.ivy

25 строки
248 B
XML

#lang ivy1.7
object t = {
type this
action a(x:this)
}
object q = {
variant this of t = struct {
b : bool
}
action a(x:this) = {
}
}
action a(x:t) = {
assume true;
call x.a;
assert false
}
export a