bool 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def x:AB(x) == x:AB(x)

is mentioned by

Thm* x,y:AP:(AProp), i,j:.
Thm* P(if i=j x else y fi)  P(if i=j x else y fi)
[eq_int_cases_test]
Thm* i,j:. (i=j) = true  i = j[eq_int_eq_true_elim]
Thm* i,j:. (i=j) = false  i  j[eq_int_eq_false_elim]
Thm* i,j:i = j  (i=j) = true[eq_int_eq_true]
Thm* i,j:i  j  (i=j) = false[eq_int_eq_false]
Thm* f:(ST), b:p,q:Sf(if b p else q fi) = if b f(p) else f(q) fi[fun_thru_ite]
Thm* b:x,y:Tb  if b x else y fi = x[ite_rw_true]
Thm* b:x,y:Tb  if b x else y fi = y[ite_rw_false]
Thm* n:i:{1..n}. 0 = 0 & n = 0  False[ite_rw_test]
Thm* x,y:xy  xy[assert_of_le_int]
Thm* p,q:pq  (p  q)[assert_of_bimplies]
Thm* p,q:. (p  q p  q[assert_of_bor]
Thm* p,q:. (pq p & q[assert_of_band]
Thm* p:p  p[assert_of_bnot]
Thm* p,q:p=q  p = q[assert_of_eq_bool]
Thm* x,y:x=y  x = y[assert_of_eq_int_rw]
Thm* x,y:x<y  x<y[assert_of_lt_int]
Thm* x,y:Atom. x=yAtom  x  y[neg_assert_of_eq_atom]
Thm* x,y:x=y  x  y[neg_assert_of_eq_int]
Thm* x,y:x=y  x = y[assert_of_eq_int]
Thm* x,y:Atom. x=yAtom  x = y[assert_of_eq_atom]
Thm* a,b:. (a  b a = b[iff_imp_equal_bool]
Thm* b:. Dec(b)[decidable__assert]
Thm* b:b = false  b[eqff_to_assert]
Thm* b:b = true  b[eqtt_to_assert]
Thm* b:b  b = false[not_assert_elim]
Thm* b:b  b = true[assert_elim]
Thm* u:. (utrue) = u[band_tt_simp]
Thm* u:. (ufalse) = false[band_ff_simp]
Thm* u:. (u  true) = true[bor_tt_simp]
Thm* u:. (u  false) = u[bor_ff_simp]
Thm* u,v:uv  u  v[assert_functionality_wrt_bimplies]
Thm* u,v,w:uv  vw  uw[bimplies_transitivity]
Thm* u,v:u = v  uv[bimplies_weakening]
Thm* i,j:ij = (j<i)[bnot_of_le_int]
Thm* p,q:(p  q) = (pq)[bnot_thru_bor]
Thm* p,q:(pq) = (p  q)[bnot_thru_band]
Thm* p:p = p[bnot_bnot_elim]
Thm* a,b:. Dec(a = b)[decidable__equal_bool]
Thm* P:(Prop). P(false P(true (b:P(b))[bool_ind]
Thm* b:b = true  b = false[bool_cases]
Thm* b:. 0b2i(b) & b2i(b)1[b2i_bounds]
Thm* b:A:Type, p,q:A. if b p else q fi  A[ifthenelse_wf]

In prior sections: core well fnd int 1

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

bool 1 Sections StandardLIB Doc