Appendix B: Converting to from Lambda--prl

This appendix discusses the differences in the Lambda--prl and Nuprl logics and user interfaces and ways to simulate Lambda--prl constructs in Nuprl .

• Differences in the Logic
  • Introduction Rules
  • Elimination Rules
  • Equality and Simplification Rules
• Differences in the User Interfaces
• Simulating Lambda--prl Constructs in Nuprl
  • Logical Operators
  • Lists
  • Primitive Recursive Functions
  • Extraction Terms