WhoCites Definitions mb automata 4 Sections GenAutomata Doc

Who Cites relname mng?
relname_mngDef [[rn]] rho e == Case(rn) Case eq(Q) = > x,y. x = y [[Q]] rho Case R = > e.R Default = > True
st_mng Def [[s]] rho == t_iterate(st_lift(rho);x,y. xy;s)
Thm* rho:Decl, s:SimpleType. [[s]] rho Type
t_iterate Def t_iterate(l;n;t) == Case(t) Case x;y = > n(t_iterate(l;n;x),t_iterate(l;n;y)) Case tree_leaf(x) = > l(x) Default = > True (recursive)
Thm* E,A:Type, l:(EA), n:(AAA), t:Tree(E). t_iterate(l;n;t) A
case_default Def Default = > body(value,value) == body
r_select Def r.l == r(l)
Thm* d:Decl, r:{d}, l:Label. r.l d(l)
case_relname_other Def Case x = > body(x) cont(x1,z) == (x1.inr(x2) = > body(hd([x2 / tl(x1)])) cont(hd(x1),z))([x1])
case_relname_eq Def Case eq(x) = > body(x) cont(x1,z) == InjCase(x1; x2. body(x2); _. cont(z,z))
case Def Case(value) body == body(value,value)
hd Def hd(l) == Case of l; nil "?" ; h.t h
Thm* A:Type, l:A List. ||l||1 hd(l) A
Thm* A:Type, l:A List. hd(l) A
tl Def tl(l) == Case of l; nil nil ; h.t t
Thm* A:Type, l:A List. tl(l) A List
case_inr Def inr(x) = > body(x) cont(value,contvalue) == InjCase(value; _. cont(contvalue,contvalue); x. body(x))
st_lift Def st_lift(rho)(x) == InjCase(x; x'. rho(x'); a. Top)
Thm* rho:(LabelType). st_lift(rho) (Label+Unit)Type
top Def Top == Void given Void
Thm* Top Type
case_tree_leaf Def Case tree_leaf(x) = > body(x) cont(x1,z) == InjCase(x1; x2. body(x2); _. cont(z,z))
case_node Def Case x;y = > body(x;y) cont(x1,z) == InjCase(x1; _. cont(z,z); x2. x2/x3,x2@0. body(x3;x2@0))

Syntax:[[rn]] rho e has structure: relname_mng(rn; rho; e)

About:
spreadlistconsconsnil
list_indunitvoidnatural_number
tokenuniondecideisectlambda
applyfunctionrecursive_def_noticeuniverseequalmembertopimplies
trueall!abstraction

WhoCites Definitions mb automata 4 Sections GenAutomata Doc