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.
Example
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.
LEGO Team
Last modified: Tue Jun 23 16:23:07 BST 1998