module Definitions: sig
.. end
type
cluster
val dummy : unit -> cluster
val cluster : id:string ->
?title:string ->
?position:Filepath.position -> unit -> cluster
val axiomatic : Wp.LogicUsage.axiomatic -> cluster
val section : Wp.LogicUsage.logic_section -> cluster
val compinfo : Cil_types.compinfo -> cluster
val matrix : unit -> cluster
val cluster_id : cluster -> string
val cluster_title : cluster -> string
val cluster_position : cluster -> Filepath.position option
val cluster_age : cluster -> int
val cluster_compare : cluster -> cluster -> int
val pp_cluster : Stdlib.Format.formatter -> cluster -> unit
val iter : (cluster -> unit) -> unit
type
trigger = (Wp.Lang.F.var, Wp.Lang.lfun) Qed.Engine.ftrigger
type
typedef = (Wp.Lang.F.tau, Wp.Lang.field, Wp.Lang.lfun) Qed.Engine.ftypedef
type
dlemma = {
}
type
definition =
type
recursion =
type
dfun = {
}
module Trigger: sig
.. end
val find_symbol : Wp.Lang.lfun -> dfun
- Raises
Not_found
if symbol is not compiled (yet)
val define_symbol : dfun -> unit
val update_symbol : dfun -> unit
val find_name : string -> dlemma
val find_lemma : Wp.LogicUsage.logic_lemma -> dlemma
- Raises
Not_found
if lemma is not compiled (yet)
val compile_lemma : (Wp.LogicUsage.logic_lemma -> dlemma) ->
Wp.LogicUsage.logic_lemma -> unit
val define_lemma : dlemma -> unit
val define_type : cluster -> Cil_types.logic_type_info -> unit
val call_fun : result:Wp.Lang.F.tau ->
Wp.Lang.lfun ->
(Wp.Lang.lfun -> dfun) ->
Wp.Lang.F.term list -> Wp.Lang.F.term
val call_pred : Wp.Lang.lfun ->
(Wp.Lang.lfun -> dfun) ->
Wp.Lang.F.term list -> Wp.Lang.F.pred
type
axioms = cluster * Wp.LogicUsage.logic_lemma list
class virtual visitor : cluster ->
object
.. end