mb label Sections GenAutomata Doc

Def l1 = l2 == Case(l1) Case ptn_atom(x) = > Case(l2) Case ptn_atom(y) = > x=yAtom Default = > false Case ptn_int(x) = > Case(l2) Case ptn_int(y) = > x=y Default = > false Case ptn_var(x) = > Case(l2) Case ptn_var(y) = > x=yAtom Default = > false Case ptn_pr( < x, y > ) = > Case(l2) Case ptn_pr( < u, v > ) = > x = uy = v Default = > false Default = > false (recursive)

is mentioned by

Thm* l1,l2:Label. l1 = l2 l1 = l2[eq_lbl_iff]
Thm* l1,l2:Label. l1 = l2 l1 = l2[assert_eq_label]
Def x ls == reduce(a,b. x = a b;false;ls)[lbls_member]

In prior sections: mb basic

Try larger context: GenAutomata

mb label Sections GenAutomata Doc