%thaw

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 STELF is in unsafe mode, the following code can be run to demonstrate %thaw:

%sort nat %.
%term z nat %.
%term s %pi nat %-> nat %.
%freeze nat %.

With nat frozen, it’s impossible to extend nat without error.

veryS: nat -> nat -> nat.

Because the STELF Wiki runs in safe mode, this example won’t work, but if you click the elf’s hat to run this code in the live STELF editor, you can toggle unsafe mode and see that %thaw allows q to be defined as a new nat.

%thaw nat.
q : nat.

See also

• %freeze