Who Cites enum1 switch?
enum1_switch	Def enum1_switch(value;el1;el2;el3) Def == Switch(value) Def == Case enum1_el1 => el1 Def == Case enum1_el2 => el2 Def == Case enum1_el3 => el3 Def == EndSwitch
switch_done	Def EndSwitch(x) == !undefined
enum1_el3	Def enum1_el3 == 2
	Thm* enum1_el3  enum1()
	Thm* enum1_el3
switch_case	Def Case v => case cont(x) == if x=v case else cont(x) fi
enum1_el2	Def enum1_el2 == 1
	Thm* enum1_el2  enum1()
	Thm* enum1_el2
enum1_el1	Def enum1_el1 == 0
	Thm* enum1_el1  enum1()
	Thm* enum1_el1
switch	Def Switch(t) b == b(t)
eq_int	Def i=j == if i=j true ; false fi
	Thm* i,j:. (i=j)

Syntax:

enum1_switch(value;el1;el2;el3)

has structure:

enum1_switch(value; el1; el2; el3)

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html