The Rules

• Semantics
  • Substitution
  • The Computation System
  • The Type System
  • Judgements
• The Type System in Detail
  • Formal Definition of Equality
  • Typehood and Membership
• The Rules
  • The Form of a Rule
  • Organization of the Rules
  • Specifying a Rule
  • Optional Parameters and Defaults
  • Hidden Assumptions
  • Shortcuts in the Presentation
• ATOM
• VOID
• INT
• LESS
• LIST
• UNION
• FUNCTION
• PRODUCT
• QUOTIENT
• SET
• EQUALITY
• UNIVERSE
• MISCELLANEOUS
• ML Constructors
• ATOM
• VOID
• INT
• LESS
• LIST
• UNION
• FUNCTION
• PRODUCT
• QUOTIENT
• SET
• EQUALITY
• UNIVERSE
• MISCELLANEOUS