CASL/Summary -- 2.2.2 Local Variable Declarations

Go backward to 2.2.1 Global Variable Declarations
Go up to 2.2 Variables

2.2.2 Local Variable Declarations

  LOCAL-VAR-AXIOMS ::= local-var-axioms VAR-DECL+ AXIOM+

A localization LOCAL-VAR-AXIOMS of variable declarations to a list of axioms is written:

vars VD₁; ...; VD_n · F₁ ... · F_m;

The sign displayed as ` · ' may be input as `·' in ISO Latin-1, or as `.' in ASCII.

It declares variables for local use in the axioms F₁, ..., F_m, but it does not contribute to the declared signature. A local declaration of a variable is equivalent to adding a universal quantification on that variable to all the indicated axioms.

CoFI Document: CASL/Summary --Version 0.99-- 21 April 1998.
Comments to cofi-language@brics.dk