Core.RefineState
module D = CodeUnit.Domain
val init : Bantorra.Manager.library -> t
val get_lib : t -> Bantorra.Manager.library
val transform_view :
shadowing:bool ->
Namespace.pattern ->
t ->
(t, 'error) Namespace.result
val transform_export :
shadowing:bool ->
Namespace.pattern ->
t ->
(t, 'error) Namespace.result
val export_view :
shadowing:bool ->
Namespace.pattern ->
t ->
(t, 'error) Namespace.result
val import :
shadowing:bool ->
Namespace.pattern ->
CodeUnit.CodeUnitID.t ->
t ->
(t, 'error) Namespace.result
val end_section :
shadowing:bool ->
prefix:Namespace.path option ->
t ->
(t, 'error) Namespace.result
val add_global :
unfolder:CodeUnit.Global.t option ->
shadowing:bool ->
Ident.t ->
D.tp ->
t ->
(CodeUnit.Global.t * t, 'error) Namespace.result
val get_global : CodeUnit.Global.t -> t -> D.tp
val resolve_global : Ident.t -> t -> CodeUnit.Global.t option
val get_global_cof_thy : t -> CodeUnit.CofThy.Disj.t
val begin_unit : Bantorra.Manager.library -> CodeUnit.id -> t -> t
Create and add a new code unit.
val loading_status :
CodeUnit.CodeUnitID.t ->
t ->
[ `Loaded | `Loading | `Unloaded ]
Add a code unit as an import.