mb
automata
4
Sections
GenAutomata
Doc
Def
tc_vc(v;ds;da;de) == Case(v) Case vc_imp(hc) = > tc_pred(hc.hyp;ds; < > ;de) & tc_pred(hc.concl;ds; < > ;de) Case vc_qimp(qhc) = > tc_pred(qhc.hyp;ds;dec_lookup(da;qhc.lbl);de) & tc_pred(qhc.concl;ds;dec_lookup(da;qhc.lbl);de) Default = > False
is mentioned by
Thm*
v:vc{i:l}(), ds,da:Collection(dec()), de:sig(), rho:Decl, e:{[[de]] rho}, s:{[[ds]] rho}, tr:trace_env([[da]] rho). tc_vc(v;ds;da;de)
trace_consistent_vc(rho;da;tr.proj;v)
vc_mng(v;rho;ds;da;de;e;s;tr)
Prop
[vc_mng_wf]
Def
tc_vcs{i}(vs;ds;da;de) ==
v:vc{i:l}(). v
vs
tc_vc(v;ds;da;de)
[tc_vcs]
Try larger context:
GenAutomata
mb
automata
4
Sections
GenAutomata
Doc