USING-COMPUTED-HINTS

Major Section:  MISCELLANEOUS

Computed hints are extraordinarily powerful. We show a few examples here to illustrate their use. We recommend that these be read in the following sequence:

• ADD-DEFAULT-HINTS -- add to the default hints

• REMOVE-DEFAULT-HINTS -- remove from the default hints

• SET-DEFAULT-HINTS -- set the default hints

• USING-COMPUTED-HINTS-1 -- Driving Home the Basics

• USING-COMPUTED-HINTS-2 -- One Hint to Every Top-Level Goal in a Forcing Round

• USING-COMPUTED-HINTS-3 -- Hints as a Function of the Goal (not its Name)

• USING-COMPUTED-HINTS-4 -- Computing the Hints

• USING-COMPUTED-HINTS-5 -- Debugging Computed Hints

• USING-COMPUTED-HINTS-6 -- Using the computed-hint-replacement feature

• USING-COMPUTED-HINTS-7 -- Using the stable-under-simplificationp flag

• USING-COMPUTED-HINTS-8 -- Some Final Comments