is mentioned by
Thm* x:Label, r:rel(). (x rel_vars(r)) (i:. i < ||r.args|| & (x term_vars(r.args[i]))) | [member_rel_vars] |
Thm* c1,c2:Collection(SimpleType), s:SimpleType. s st_app(c1;c2) (a:SimpleType. a c2 & as c1) | [member_st_app] |
Thm* a,b:Term List. a = b ||a|| = ||b|| (i:. i < ||a|| & a[i] = b[i]) | [unequal_termlists] |
Def pred_mentions(p;x) == r:rel(). r p & rel_mentions(r;x) | [pred_mentions] |
Def rel_mentions(r;x) == i:. i < ||r.args|| & (x term_vars(r.args[i])) | [rel_mentions] |
Def covers_var(A;x) == fr:frame(). fr < fr A.frame | fr.var = x > & (a:Label. (a fr.acts) (ef:eff(). ef < ef A.eff | ef.kind = a & ef.smt.lbl = x > )) | [covers_var] |
In prior sections: core fun 1 int 2 mb nat num thy 1 mb list 1 mb collection mb list 2
Try larger context:
GenAutomata