Module Core.RefineState

module D = CodeUnit.Domain
type t
val init : Bantorra.Manager.library -> t
val get_lib : t -> Bantorra.Manager.library
val get_holes : t -> (D.tp * D.cof * D.tm_clo) list
val add_hole : (D.tp * D.cof * D.tm_clo) -> t -> t
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 begin_section : t -> t
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 end_unit : parent:t -> child:t -> t
val loading_status : CodeUnit.CodeUnitID.t -> t -> [ `Loaded | `Loading | `Unloaded ]

Add a code unit as an import.