Definitions mb record GenAutomata Doc

Defined Operators mentioned in mb record (and any they in turn depend on)

Defr.l[r_select]
Defkind(a)[kind]
Defvalue(a)[value]
Def{p}[record_pair]
DefD(i) for i I[dall]mb declaration
DefDecl[decl]mb declaration
Defx:A. B(x)[all]core
Def(d)[sigma]
Def{d}[record]
Defdecl_type(d;x)[decl_type]mb declaration
DefLabel[lbl]mb label
Def1of(t)[pi1]core
Def2of(t)[pi2]core
Defground_ptn(p)[ground_ptn]mb basic
Defb[assert]bool 1
DefPattern[ptn]mb basic
DefDefault = > body[case_default]prog 1
Defpq[band]bool 1
DefCase ptn_pr( < x, y > ) = > body(x;y) cont[case_lbl_pair]mb basic
DefCase ptn_var(x) = > body(x) cont[case_ptn_var]mb basic
DefCase(value) body[case]prog 1
Defptn_con(T)[ptn_con]mb basic
Defhd(l)[hd]list 1
Deftl(l)[tl]list 1
Definl(x) = > body(x) cont[case_inl]prog 1
Definr(x) = > body(x) cont[case_inr]prog 1

About:
spreadspreadspreadproductproductconsconsnil
list_indbfalsebtrueifthenelse
assertintatomtokenuniondecideset
isectlambdaapplyfunctionycombrecuniversefalsetrue
all

Definitions mb record GenAutomata Doc