u:Term, te:(Label
Label
), e,s,a:Top.
[[u]] e s a mk_trace_env(nil, te) ~ [[u]] e s a niltrace()is mentioned by
|
Thm* u:Term, te:(LabelLabel), e,s,a:Top.
[[u]] e s a mk_trace_env(nil, te) ~ [[u]] e s a niltrace() | [term_mng_nil] |
| Thm* SQType(Term) | [term_sq2] |
Try larger context: GenAutomata