Go backward to Signature Declarations
Go up to Basic Constructs
Go forward to Axioms and Terms

Variable Declarations

  VAR-DECL         ::=  var-decl VAR+ SORT
  VAR              ::=  SIMPLE-ID
A variable declaration VAR-DECL determines sorted variables for use in axioms; it does not contribute to the signature. Such a declaration of a variable as a BASIC-ITEM abbreviates adding a universal quantification on that variable to all axioms in the enclosing BASIC-SPEC. Note that universal quantification over a variable that does not occur free in an axiom is semantically irrelevant.
CoFI Document: LanguageSummary --DRAFT, Version 0.96-- 30 April 1997.
Comments to cofi-language@brics.dk