Definitions hol pair Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
his_pairDef is_pair == p:'a'bx:'ay:'b. (p = (mk_pair(x,y)))
Thm* 'a,'b:S. is_pair  (('a  'b  hbool)  hbool)
type_definitionDef type_definition('a;'b;P;rep)
Def == (x',x'':'brep(x') = rep(x'' 'a  x' = x'')
Def == & (x:'a(P(x))  (x':'bx = rep(x')))
Thm* 'a,'b:Type, P:('a), rep:('b'a). type_definition('a;'b;P;rep Prop
assertDef b == if b True else False fi
Thm* b:b  Prop
hboolDef hbool == 
Thm* hbool  S
hprodDef hprod('a'b) == 'a'b
Thm* 'a,'b:S. hprod('a'b S
hrep_prodDef rep_prod == p:'a'b. mk_pair(1of(p),2of(p))
Thm* 'a,'b:S. rep_prod  (hprod('a'b 'a  'b  hbool)
stypeDef S == {T:Type| x:T. True }
Thm* S  Type{2}

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

Definitions hol pair Sections HOLlib Doc