Next: Configure Equality Up: New features in LEGO Version 1.3

LEGO Version 1.3: Assumption

The command Assumption constructs a proof term for the current goal if it is a (first-order) instance of any of the current assumptions. Assumption RELGOAL is an abbreviation for Next RELGOAL; Assumption.


Assumption and Immed

The commands Try Assumption and Immed are equivalent in a proof state with a single visible goal. In a proof state with multiple goals, throwing Assumption at a specific goal may well be a better strategy than invoking Immed. The latter tactic may incorrectly unify some existential variables. It may also take a long time to process.

Notice that Immed never fails.

Last modified: Tue Jun 23 16:23:07 BST 1998