Who Cites his num rep?
his_num_rep	Def is_num_rep Def == m:. P: Def == m:. ((P(zero_rep))(n:. (P(n))(P(suc_rep(n)))))(P(m))
	Thm* is_num_rep  (hind  hbool)
hzero_rep	Def zero_rep == @x:. (y:. x = suc_rep(y)  )
	Thm* zero_rep  hind
hsuc_rep	Def suc_rep == x:. (@f:. (one_one(;;f) & onto(;;f)))(x)
	Thm* suc_rep  (hind  hind)
bimplies	Def pq == p  q
	Thm* p,q:. pq
nat	Def  == {i:| 0i }
	Thm*   Type
	Thm*   S
ball	Def x:T. P(x) == (x:T. P(x))
	Thm* T:Type, P:(T). (x:T. P(x))
band	Def pq == if p q else false fi
	Thm* p,q:. (pq)
tlambda	Def (x:T. b(x))(x) == b(x)
onto	Def onto('a;'b;f) == y:'b. x:'a. y = f(x)
	Thm* 'a,'b:Type, f:('a'b). onto('a;'b;f)  Prop
le	Def AB == B<A
	Thm* i,j:. (ij)  Prop
not	Def A == A  False
	Thm* A:Prop. (A)  Prop
one_one	Def one_one('a;'b;f) == x,y:'a. f(x) = f(y)  'b  x = y
	Thm* 'a,'b:Type, f:('a'b). one_one('a;'b;f)  Prop
choose	Def @x:T. P(x) == InjCase(lem({x:T| P(x) }); x. x, arb(T))
	Thm* T:S, P:(TType). (@x:T. P(x))  T
bnot	Def b == if b false else true fi
	Thm* b:. b
bor	Def p  q == if p true else q fi
	Thm* p,q:. (p  q)
assert	Def b == if b True else False fi
	Thm* b:. b  Prop
prop_to_bool	Def P == InjCase(lem(P) ; true; false)
	Thm* P:Prop. (P)
arb	Def arb(T) == InjCase(lem(T); x. x, "uu")
	Thm* T:S. arb(T)  T

Syntax:

is_num_rep

has structure:

his_num_rep

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