WhoCites Definitions mb automata 2 Sections GenAutomata Doc

Who Cites tappend?
tappendDef 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 LabelLabel
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:AB(a)). 2of(p) B(1of(p))
pi1 Def 1of(t) == t.1
Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A

Syntax:tappend(tr;a) has structure: tappend(tr; a)

About:
pairspreadspreadproductlistconsconsnil
list_indboolfunction
recursive_def_noticeuniversememberall!abstraction

WhoCites Definitions mb automata 2 Sections GenAutomata Doc