Def |i| == if 0i i else -i fi

is mentioned by

Thm* WellFnd{i}(;x,y.|x|<|y|)	[int_mag_well_founded]
Thm* a:, b:. |a| = |b|  (a rem b) = 0	[rem_eq_args_z]
Thm* a:, b:. |a|<|b|  (a rem b) = a	[rem_base_case_z]
Thm* a:, n:. |a|<|n|  (a rem n) = a	[rem_gen_base_case]
Thm* a:, n:. |a rem n|<|n|	[rem_mag_bound]
Thm* a:, b:. |a rem b|<|b|	[rem_bounds_z]
Thm* P:(Prop). (x:. P(|x|))  (x:. P(x))	[absval_elim]
Thm* i:. |i| = |-i|	[absval_sym]
Thm* x,y:. |x| = |y|  x =  y	[absval_eq]
Thm* i:, n:. |i|>n  i<-n  i>n	[absval_lbound]
Thm* i:, n:. |i|n  -ni & in	[absval_ubound]
Thm* i:. |i| = 0  i = 0	[absval_zero]
Thm* i:{...0}. |i| = -i	[absval_neg]
Thm* i:. |i| = i	[absval_pos]

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html