Origin Definitions StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Nuprl Section: core - Some basic concepts defined type-theoretically.

Selected Objects
defunit Unit == 0  
deftrue True == 0  
deffalse False == Void
defand P & Q == PQ
defor P  Q == P+Q
defimplies P  Q == PQ
defrev_implies P  Q == Q  P
defsquash T == {:True| T }
defnot A == A  False
defnequal a  b  T == a = b  T
defiff P  Q == (P  Q) & (P  Q)
defexists x:AB(x) == x:AB(x)
defsq_exists x:AB(x) == {x:AB(x) }
defall x:AB(x) == x:AB(x)
defle AB == B<A
defge ij == ji
defgt i>j == j<i
defsubtype S  T == x:Sx  T
deftop Top == Void(given Void)
COMcore_2_summary General-purpose definitions andtheorems.
COMcore_2_intro Introduces a variety of general-purpose definitions andtheorems.
definfix_ap x f y == f(x,y)
deflabel t  ...$L == t
defguard {T} == T
deferror ??? == "error"
defprop Prop == Type
defcand A & B == AB
COMCOMBS_acom Common Combinators
deficomb I(x) == x
defkcomb K(x,y) == x
defscomb S(x,y,z) == x(z,y(z))
COMPRODUCT_DEFS_acom Projection functions for pairs
defpi1 1of(t) == t.1
defpi2 2of(t) == t.2
THMpair_eta_rw B:(AType), p:(a:AB(a)). <1of(p),2of(p)> = p  a:AB(a)
defspread3 let x,y,z = a in t(x;y;z) == a/x,zzzz/y,zt(x;y;z)
defspread4 let w,x,y,z = a in t(w;x;y;z) == a/w,zz1zz1/x,zz2zz2/y,zt(w;x;y;z)
defspread5 let a,b,c,d,e = u in v(a;b;c;d;e)
== u/a,zz1zz1/b,zz2zz2/c,zz3zz3/d,ev(a;b;c;d;e)
defspread6 let a,b,c,d,e,f = u in v(a;b;c;d;e;f)
== u/a,zz1zz1/b,zz2zz2/c,zz3zz3/d,zz4zz4/e,fv(a;b;c;d;e;f)
defspread7 let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g)
== u/a,zz1.
== zz1/b,zz2zz2/c,zz3zz3/d,zz4zz4/e,zz5zz5/f,gv(a;b;c;d;e;f;g)
COMUNIT_DEFS_acom Inhabitant of Unit type
defit  == *
THMunit_triviality a:Unit. a = 
COMCONSTR_PROPERTIES_com Predicates for constructive properties of propositions, andlemmas characterizing how these predicates are inherited.Worthwhile sometime redoing thms for soft abstractionsin terms of the underlying hard abstractions / primitives.
defdecidable Dec(P) == P  P
THMdecidable__or Dec(P Dec(Q Dec(P  Q)
THMdecidable__and Dec(P Dec(Q Dec(P & Q)
THMdecidable__implies Dec(P Dec(Q Dec(P  Q)
THMdecidable__false Dec(False)
THMdecidable__iff Dec(P Dec(Q Dec(P  Q)
THMdecidable__int_equal i,j:. Dec(i = j)
THMdecidable__atom_equal a,b:Atom. Dec(a = b)
THMiff_preserves_decidability Dec(A (A  B Dec(B)
defstable Stable{P} == P  P
THMstable__not Stable{P}
THMstable__function_equal f,g:(AB). (x:A. Stable{f(x) = g(x)})  Stable{f = g}
THMstable__from_decidable Dec(P Stable{P}
defsq_stable SqStable(P) == P  P
THMsq_stable__and SqStable(P SqStable(Q SqStable(P & Q)
THMsq_stable__implies SqStable(Q SqStable(P  Q)
THMsq_stable__iff SqStable(P SqStable(Q SqStable(P  Q)
THMsq_stable__all P:(AProp). (x:A. SqStable(P(x)))  SqStable(x:AP(x))
THMsq_stable__equal x,y:A. SqStable(x = y)
THMsq_stable__squash SqStable(P)
THMsq_stable__from_stable Stable{P SqStable(P)
THMsq_stable__not SqStable(P)
THMsq_stable_from_decidable Dec(P SqStable(P)
defxmiddle XM == P:Prop. Dec(P)
THMsquash_elim SqStable(P (P  P)
COMLOGIC_THMS_tcom Theorems of inituitionistic propositional and predicate logic.
THMdneg_elim Dec(A A  A
THMdneg_elim_a Dec(A (A  A)
THMiff_symmetry (A  B (B  A)
THMand_assoc A & (B & C (A & B) & C
THMand_comm A & B  B & A
THMor_assoc A  (B  C (A  B C
THMor_comm A  B  B  A
THMnot_over_or (A  B A & B
THMnot_over_or_a (A  B A & B
THMnot_over_and_b A  B  (A & B)
THMnot_over_and Dec(A ((A & B A  B)
THMand_false_l False & A  False
THMand_false_r A & False  False
THMand_true_l True & A  A
THMand_true_r A & True  A
THMor_false_l False  A  A
THMor_false_r A  False  A
THMor_true_l True  A  True
THMor_true_r A  True  True
THMexists_over_and_r B:(TProp). (x:TA & B(x))  A & (x:TB(x))
THMnot_over_exists Q:(TProp). (x:TQ(x))  (x:TQ(x))
COMEQUALITY_THMS_tcom Equality Theorems
COMREWRITE_SUPPORT_tcom Lemma support for rewriting.
THMiff_transitivity (P  Q (Q  R (P  R)
THMimplies_transitivity (P  Q (Q  R P  R
THMand_functionality_wrt_iff (P1  P2 (Q1  Q2 (P1 & Q1  P2 & Q2)
THMand_functionality_wrt_implies (P1  P2 (Q1  Q2 P1 & Q1  P2 & Q2
THMimplies_functionality_wrt_iff (P1  P2 (Q1  Q2 ((P1  Q1 (P2  Q2))
THMimplies_functionality_wrt_implies (P1  P2 (Q1  Q2 (P1  Q1 P2  Q2
THMdecidable_functionality (P  Q (Dec(P Dec(Q))
THMiff_functionality_wrt_iff (P1  P2 (Q1  Q2 ((P1  Q1 (P2  Q2))
THMall_functionality_wrt_iff P,Q:(SProp). S = T  (x:SP(x Q(x))  ((x:SP(x))  (y:TQ(y)))
THMall_functionality_wrt_implies P,Q:(SProp). S = T  (z:SP(z Q(z))  (x:SP(x))  (y:TQ(y))
THMexists_functionality_wrt_iff P,Q:(SProp). S = T  (x:SP(x Q(x))  ((x:SP(x))  (y:TQ(y)))
THMexists_functionality_wrt_implies P,Q:(SProp). S = T  (x:SP(x Q(x))  (x:SP(x))  (y:TQ(y))
THMnot_functionality_wrt_iff (P  Q (P  Q)
THMnot_functionality_wrt_implies (P  Q P  Q
THMor_functionality_wrt_iff (P1  P2 (Q1  Q2 (P1  Q1  P2  Q2)
THMor_functionality_wrt_implies (P1  P2 (Q1  Q2 P1  Q1  P2  Q2
THMsquash_functionality_wrt_implies (P  Q P  Q
THMsquash_functionality_wrt_iff (P  Q (P  Q)
THMimplies_antisymmetry (P  Q (Q  P (P  Q)
COMMISC_DEFS_com Miscellaneous General Definitions
deflet let x = a in b(x) == (x.b(x))(a)
COMtype_inj_acom type_inj is intended chiefly for injecting into quotienttypes. For convenience, typing lemmas should be provenfor each application. e.g. ... x:T. [x]{a,b:T//Eab}A general typing lemma for type_inj(x;T) cannotbe proven, because it's antecedent would involve the subtypepredicate which isn't typeable.
deftype_inj [x]{T} == x
THMfun_thru_spread B:(AType), p:(x:AB(x)), C,D:Type, f:(CD), b:(x:AB(x)C).
f(p/x,yb(x,y)) = (p/x,yf(b(x,y)))
THMspread_to_pi12 B:(AType), p:(x:AB(x)), C:Type, b:(x:AB(x)C).
(p/x,yb(x,y)) = b(1of(p),2of(p))
defsingleton {a:T} == {x:Tx = a  T }
THMsingleton_properties a:Tx:{a:T}. x = a  T
defunique_set {!x:T | P(x)} == {x:TP(x) & (y:TP(y y = x) }
defuni_sat a = !x:TQ(x) == Q(a) & (a':TQ(a' a' = a)
THMuni_sat_imp_in_uni_set a:TQ:(TProp). (a = !x:TQ(x))  a  {!x:T | Q(x)}
defycomb Y(f) == (x.f(x(x)))(x.f(x(x)))
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Origin Definitions StandardLIB Doc