P,k. false
)
d:Decl. niltrace() 
trace_env(d)d:Decl, trace:(
d) List, proj:(Label
Label
). mk_trace_env(trace, proj) trace_env(d)| Who Cites niltrace? | |
| niltrace | Def niltrace() == mk_trace_env(nil, P,k. false) |
| Thm* d:Decl. niltrace() trace_env(d) | |
| mk_trace_env | Def mk_trace_env(trace, proj) == < trace,proj > |
| Thm* d:Decl, trace:(d) List, proj:(LabelLabel). mk_trace_env(trace, proj) trace_env(d) |
| Syntax: | niltrace() | has structure: | niltrace |
About:
 |  |  |  |  |  |  |  |  |  |