Summary
- examples and documentation for code generator time measurements
- optional timing for code generator conversions
- clarified internal interfaces
- tuned
- delegate inclusion of required dictionaries to user-space instead of half-working magic
- corrected closure scope of static_conv_thingol; clarified implementation and names
- clarified proof context vs. background theory
- explicit quasi-global context for nbe conversions -- works around quasi-global type variable handling in lift_triv_classes_conv
- clarified naming conventions and code for code evaluation sandwiches
- clarified names of variants