8.2.1 Metavariables

Prev Up Next Page 304 of 800 Search internet

A construct is considered to be a metavariable if its 'meta/kg' aspect is the string 'var'. Thus, you can construct a metavarible just by defining a new construct and by defining the 'meta/kg' aspect of your construct as 'var'. The following construct allows to declare a construct to be a metavariable:

macro define metadeclare x as meta define x as "var" end define end define

macro define meta define x as y end define as define meta of x as y end define end define

eager message define meta as "meta/kg" end define

You cannot declare constructs from other pages to be metavariables. Constructs can only be declared to be metavariables on their home page, i.e. on the page on which the construct is defined.

The check page declares #a ,, #b ,, #c ,, ... as metavariables.

When the Logiweb proof checker needs to know whether or not a construct is a metavariable, it inspects the domestic 'meta/kg' aspect of the construct. A domestic aspect of a construct is one which is defined on the constructs home page.

The aspect name 'meta/kg' contains a slash and, thus, it is non-reserved. It would have been a violation of conventions to call the aspect something like 'meta' because 'meta' is reserved for future extensions of Logiweb.

The Logiweb proof checker comes with the Logiweb package as an example of how one can express a proof checker. The proof checker is not a part of the Logiweb system, and thus it is not allowed to use reserved aspects.

An aspect is reserved iff it consists of nothing but reserved characters. A character is reserved if it is one of the small letters a-z of the Latin alphabet or a space character. More precisely, Unicodes 97-122 as well as Unicode 32 are reserved. An aspect is non-reserved if it contains at least one non-reserved character.

Prev Up Next Page 304 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05