Subject: Fragments

Keywords: ::dbbot
          ::tnf

Title: tnf bot

--------------------------------------------------
ThenNormalForm :
 Normalize Tactic expression so that it can be easily dekreitzed.

Sent to dialog if refine fails or produces unexpected subgoal.
  - producing fewer subgoals is OK.

One odd thing is that dialog proof uses orig tactic and not the 
then normalized tactic. If dialog is exited then does use tnf from 
dialog but doesn't refine it, ie assumes it will work since good exit.
Should use tnf in dialog prf.

tnf is stored as property in source record.
 includes an oriqeq flag and a verify flag.
   - origeq is true if tnf doesn't differ from orig tactic.
   - verify is true if tnf refines similarly to orig.

fail  - sets verified flag in tnf prop to false
exit  - save tnf from dialog and set verify flag true
retry
defer  

HPF happens somehow too? ⋅
--------------------------------------------------

Authors: 

Contributors: NUPRL:t

⋅

Home