Origin Definitions Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
sqequal_1
Nuprl Section: sqequal_1

Selected Objects
COMsqequal_com Here are the essentials: ...
COMsq_type_com There are other types in Nuprl that we can consider first order types. ...
defsq_type SQType(T) == x,y:Tx = y  {x ~ y}
THMint_sq SQType()
THMnat_sq SQType()
THMbool_sq SQType()
THMatom_sq SQType(Atom)
THMbool_sim_true b:b = true  (b ~ true)
THMbool_sim_false b:b = false  (b ~ false)
THMeq_int_eq_true_intro i,j:i = j  ((i=j) ~ true)
THMeq_int_eq_false_intro i,j:i = j  ((i=j) ~ false)
THMlt_int_eq_true_elim i,j:. (i<j) = true  i<j
THMlt_int_eq_false_elim i,j:. (i<j) = false  i<j
THMeq_atom_eq_true_elim x,y:Atom. x=yAtom = true  x = y
THMeq_atom_eq_false_elim x,y:Atom. x=yAtom = false  x = y
THMeq_int_eq_true_elim_sqequal i,j:. ((i=j) ~ true i = j
THMeq_int_eq_false_elim_sqequal i,j:. ((i=j) ~ false i  j
THMlt_int_eq_true_elim_sqequal i,j:. ((i<j) ~ true i<j
THMlt_int_eq_false_elim_sqequal i,j:. ((i<j) ~ false i<j
THMeq_atom_eq_true_elim_sqequal x,y:Atom. (x=yAtom ~ true x = y
THMeq_atom_eq_false_elim_sqequal x,y:Atom. (x=yAtom ~ false x = y
THMbool_cases_sqequal b:. (b ~ true (b ~ false)
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Origin Definitions Sections StandardLIB Doc