From The Twelf Project
Jump to: navigation, search
This article or section describes an undocumented feature of Twelf.
The information may be incomplete and subject to change.

The %thaw directive allows previously frozen type families to be extended with new canonical forms. Because this can easily be used to invalidate metatheorems, it is a directive that can only be used in unsafe mode.

If Twelf is in unsafe mode, the following code can be run to demonstrate %thaw:

nat : type.
z : nat.
s : nat -> nat.

%freeze nat.

% Right here I could not declare a new constant of type nat

%thaw nat.

% Now I can define a wacky new natural number
q : nat.

See also