%freeze

The %freeze declaration freezes a set of type families. A frozen family cannot be extended: new constants at that type cannot be added, nor can the subordination relation be extended such that the family could depend on other types. The %thaw declaration can be used to reenable the extension of a type family.

Syntax

The syntax is as follows:

%freeze t1 t2 ... tn.

The type families t1–tn are frozen.

Example

Suppose we define addition in the natural way:

%sort nat %.
%term z nat %.
%term s %pi nat %-> nat %.
%prec %prefix 9999 s %.
%sort plus {_ nat} {_ nat} {_ nat} %.
%mode plus %in %in %out %.
%term plus/z plus z N N %.
%term plus/s %pi (plus (s N) M (s P)) %<- (plus N M P) %.

At this point, we may still extend the definition of addition:

plus/zz : plus M z M.

However, if we freeze plus then this will not be allowed:

%freeze plus.
plus/zzz : plus z z z.

More subtly, we will not be able to extend the subordination relation for plus:

%freeze plus.
thing : type.

oops : (thing -> plus _ _ _) -> type.

The subordination relation can be extended such that other non-frozen types depend on a frozen type: we can make a new thing depend on plus, just not the other way around.

%freeze plus.
thing : type.

okay : (plus _ _ _ -> thing) -> type.

Autofreeze

Because types are automatically frozen for any family for which there has been a %worlds declaration, or for any type family that depends on that family. This prevents mistakes where a metatheorem is proved for a type family but then that type family is extended, invalidating the theorem.