%thaw
From The Twelf Project
| 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.
