Definitions DiscreteMath DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Defined Operators mentioned in DiscreteMath

Def  seq:l[list_to_function]
Def  find_first_iter(v.p(v); v.f(v); a)[find_first_iter]
Def  f is permutation on A[is_permutation]
Def  fin_enum(A)[fin_enum]
Def  Nil[seq_nil]
Def  [xxs][seq_cons]
Def  xs[list_member_type]
Def  1-1-Corr x:A,y:BR(x;y)[is_one_one_corr_rel]
Def  Prop[prop]core
Def  a -- b[ndiff]int 2
Def  AB[isect_two]LogicSupplement
Def  Finite(A)[is_finite_type]
Def  Unbounded(A)[unboundedly_infinite]
Def  Infinite(A)[productively_infinite]
Def  a {k} T[sized_mset]
Def  {i...}[int_upper]int 1
Def  a {k} [sized_bool]
Def  [nat]int 1
Def  {i..j}[int_seg]int 1
Def  {i...j}[int_iseg]int 1
Def  i  j < k[lelt]int 1
Def  AB[le]core
Def  IsEqFun(T;eq)[eqfun_p]rel 1
Def  A Discrete[is_discrete]LogicSupplement
Def  Dec(P)[decidable]core
Def  {a:T}[singleton]core
Def  A =ext B[exteq]LogicSupplement
Def  A bij B[bijection_type]
Def  !A[inhabited_uniquely]LogicSupplement
Def  S  T[subtype]core
Def  [nat_plus]int 1
Def  A onto B[surjection_type]
Def  A & B[cand]core
Def  a  b[nequal]core
Def  1-1 xA,yBR(x;y)[rel_1_1_b]
Def  R is 1-1[rel_1_1]
Def  SqStable(P)[sq_stable]core
Def  least i:p(i)[least]
Def  b[assert]bool 1
Def  x f y[infix_ap]core
Def  EquivRel on AR[equiv_rel_sep]LogicSupplement
Def  EquivRel x,y:TE(x;y)[equiv_rel]rel 1
Def  Trans x,y:TE(x;y)[trans]rel 1
Def  T[squash]core
Def  (x:AB(x)) ~ (x':A'B'(x'))[one_one_corr_fams]
Def  union_to_sigma[union_to_sigma]
Def  sigma_to_union[sigma_to_union]
Def  k![factorial_via_iter]IteratedBinops
Def  Dedekind-Infinite(A)[Dedekind_infinite]
Def  x:A st P(x)B(x)[fun_over_st]LogicSupplement
Def  {T}[guard]core
Def  A/E[quotient_sep]LogicSupplement
Def   x:A st P(x). Q(x)[allst]LogicSupplement
Def  Unit[unit]core
Def  k!m[factorial_tail_via_iter]IteratedBinops
Def  prev_nat_pair[prev_nat_pair]
Def  nat_to_nat_pair[nat_to_nat_pair]
Def  same_range_sep(AB)[same_range_sep]
Def  !x:AP(x)[exists_unique]LogicSupplement
Def  x:AB(x)[all]core
Def  P & Q[and]core
Def  P  Q[or]core
Def  False[false]core
Def  Y[ycomb]core
Def  if b t else f fi[ifthenelse]bool 1
Def  f{i}[compose_iter]
Def  Replace value k by f(m) in f[delete_fenum_value]
Def  next_nat_pair[next_nat_pair]
Def  i=j[eq_int]bool 1
Def  P  Q[iff]core
Def  P  Q[implies]core
Def  x:AB(x)[exists]core
Def  AB[inv_pair]
Def  A inj B[injection_type]
Def  A[inhabited]LogicSupplement
Def  A[not]core
Def  size(a)[boolsize]
Def  Msize[msize]
Def  Iter(f;ui:{a..b}. e(i)[iter_via_intseg]IteratedBinops
Def  [bool]bool 1
Def  a  xs[is_list_mem]
Def  A ~ B[one_one_corr_2]
Def  A ~~ B[one_one_corr]
Def  Replace values x s.t. P(x) by y in f[replace_fn_values]
Def  InvFuns(ABfg)[inv_funs]
Def  Bij(ABf)[biject]
Def  Inj(ABf)[inject]
Def  Surj(ABf)[surject]
Def  f is 1-1 corr[is_one_one_corr]
Def  InvFuns(A;B;f;g)[inv_funs_2]
Def  l[i][select]
Def  imax(a;b)[imax]int 2
Def  Sym x,y:TE(x;y)[sym]rel 1
Def  Refl(T;x,y.E(x;y))[refl]rel 1
Def  1,2b(1;2)[so_lambda2]
Def  x is the u:AP(u)[is_the]LogicSupplement
Def  P  Q[rev_implies]core
Def  nth_tl(n;as)[nth_tl]
Def  ij[le_int]bool 1
Def  i<j[lt_int]bool 1
Def  Id[tidentity]
Def  f o g[compose]
Def  hd(l)[hd]
Def  Id[identity]
Def  tl(l)[tl]
Def  b[bnot]bool 1

About:
pairspreadproductproductnillist_ind
boolbfalsebtrueifthenelseassertunitvoidintnatural_number
addsubtractmultiplyint_eqlessless_thantokenunion
inlinrdecidesetisect
quotientlambdaapplyfunctionycombuniverseequalmembersubtype
propimpliesandorfalsetrueallexists
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Definitions DiscreteMath DiscrMathExt Doc