package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
inherit [Z.t, T.ADT.t, T.Field.t, T.Fun.t, T.tau, T.var, T.term, Env.t] Qed.Engine.engine
method marks : Env.t * T.marks
method op_spaced : string -> bool
method op_record : string * string
method pp_forall : T.tau -> string list Qed.Plib.printer
method pp_intros : T.tau -> string list Qed.Plib.printer
method pp_exists : T.tau -> string list Qed.Plib.printer
method pp_param : (string * T.tau) Qed.Plib.printer
method pp_declare_symbol : Qed.Engine.cmode -> T.Fun.t Qed.Plib.printer
method pp_declare_adt : Format.formatter -> T.ADT.t -> int -> unit
method pp_declare_def : Format.formatter -> T.ADT.t -> int -> T.tau -> unit
method pp_declare_sum : Format.formatter -> T.ADT.t -> int -> (T.Fun.t * T.tau list) list -> unit
method declare_type : Format.formatter -> T.ADT.t -> int -> typedef -> unit
method declare_prop : kind:string -> Format.formatter -> string -> T.var list -> trigger list list -> T.term -> unit
method declare_axiom : Format.formatter -> string -> T.var list -> trigger list list -> T.term -> unit
method declare_fixpoint : prefix:string -> Format.formatter -> T.Fun.t -> T.var list -> T.tau -> T.term -> unit
method declare_signature : Format.formatter -> T.Fun.t -> T.tau list -> T.tau -> unit
method declare_definition : Format.formatter -> T.Fun.t -> T.var list -> T.tau -> T.term -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct