%subord

From The Twelf Project

This article describes an undocumented feature of Twelf.
The information may be incomplete and subject to change.

The %subord declaration adds edges to the subordination relation. This declaration is currently only available in Twelf CVS^[?] and may not yet be available in TwelfTag.

[edit] Syntax

The syntax is as follows:

%subord (t1 t1') ... (tn tn').

The type families ti' will then be treated as being dependent on the type family ti.

[edit] Example

This article or section needs a good concise example..

Twelf keywords

%. %abbrev %assert %block %clause %covers %define %deterministic %establish %freeze %infix %prefix %postfix %mode %name %prove %query %querytabled %reduces %solve %subord %tabled %terminates %thaw %theorem %total %trustme %unique %use %worlds

This page is incomplete. We should expand it.

%subord

From The Twelf Project

[edit] Syntax

[edit] Example

Views

Personal tools

the twelf wiki

learn twelf

reference

Search

Toolbox