Rules

Rules of grammar are declared in the following manner:

rule wi (ph : wff, ps : wff) {
    term : wff = # ( ph → ps ) ;;
}
rule wal (ph : wff, x : set) {
    term : wff = # ∀ x ph ;;
}

rule - is a keyword for the rule construction, followed by a rule name and a list of variables. Then the body of the rule is placed in the braces. The body of the rule is started with the keyword term, which states, that the following expression is used as a term, but not as a proposition, and after a colon there is a type of the rule - it's left-side non-terminal. The string, which actually gives a right-side of the rule is placed between # and ;; keywords. When forming a rule, the names of variables are replaced with their types. So, as a grammar rules the rules given in example will be (in BNF notation):

wff ::= ( wff → wff )
wff ::= ∀ set wff