Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

is_sealed

Thm.is_sealed : string -> bool

Tests whether a theory has been sealed in the current session.

A sealed theory is locked against further change (see Thm.mark_sealed for the guarantee). The theory "min" is sealed at kernel bootstrap; a user theory becomes sealed when Theory.export_theory writes it to disk or when the theory-load machinery loads a pre-built copy into the session.

Failure

Never fails.

See also

Thm.mark_sealed, Thm.setCT