Module BaseLogic.SeparationLogic

module ID : sig ... end
val nil : t
val mk_block_begin : t -> t
val mk_block_end : t -> t
val mk_heap_term : MemoryModel0.Field.t -> t -> t
val mk_pure : t -> t
val emp : t
val mk_star : Self.t Stdlib.List.t -> Self.t
val mk_septraction : t -> t -> t
val mk_wand : t -> t -> t
val mk_pto_struct : t -> MemoryModel.StructDef.t -> t Stdlib.List.t -> t
val mk_pto_tuple : t -> t Stdlib.List.t -> t
val mk_pto : t -> t -> t
val mk_predicate : Stdlib.String.t -> ?structs:MemoryModel.StructDef.t Stdlib.List.t -> t Stdlib.List.t -> t
val mk_ls : t -> t -> t
val mk_dls : t -> t -> t -> t -> t
val mk_nls : t -> t -> t -> t
val mk_gneg : Self.t -> Self.t -> t
val is_nil : Self.t -> bool