Module notebook_elab 

Elaboration for frontend notebooks.

The notebook elaborator is disjoint from the text elaborator. One reason for this is that error reporting must be completely different to be well adapted to the notebook interface. As a first pass, we are associating cell UUIDs with errors.

Structs

Elaborator

The current state of a notebook elaboration session.

Functions

demote_modality

Demotes a modality to notebook type.

promote_modality

Promotes a modality from notebook type to modality for modal theory.