Definitions
HanoiTowers
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
eq_hanoi_PEG
Def
p
=
q
== if
p
=
q
true
; false
fi
Thm*
p
,
q
:Peg. (
p
=
q
)
hanoi_PEG
Def
Peg == {1...3}
Thm*
Peg
Type
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
HanoiTowers
Sections
NuprlLIB
Doc