| | Who Cites tappend? |
|
| tappend | Def tappend(tr;a) == mk_trace_env(tr.trace @ [a], tr.proj) |
| | | Thm*  d:Decl, tr:trace_env(d), a:( d). tappend(tr;a)  trace_env(d) |
|
| trace_env_proj | Def t.proj == 2of(t) |
| | | Thm* d:Decl, t:trace_env(d). t.proj Label  Label |
|
| trace_env_trace | Def t.trace == 1of(t) |
| | | Thm* d:Decl, t:trace_env(d). t.trace (d) List |
|
| append | Def as @ bs == Case of as; nil  bs ; a.as' [a / (as' @ bs)] (recursive) |
| | | Thm* T:Type, as,bs:T List. (as @ bs) T List |
|
| 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) |
|
| pi2 | Def 2of(t) == t.2 |
| | | Thm* A:Type, B:(AType), p:(a:A B(a)). 2of(p) B(1of(p)) |
|
| pi1 | Def 1of(t) == t.1 |
| | | Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A |
