package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Module `Qed.Kind`Source

Logic Types Utilities

Sourceval of_tau : ('f, 'a) Logic.datatype -> Logic.sort

Sourceval of_poly : (int -> Logic.sort) -> ('f, 'a) Logic.datatype -> Logic.sort

Sourceval image : Logic.sort -> Logic.sort

Sourceval degree_of_tau : ('f, 'a) Logic.datatype -> int

Sourceval degree_of_list : ('f, 'a) Logic.datatype list -> int

Sourceval degree_of_sig : ('f, 'a) Logic.funtype -> int

Sourceval type_params : int -> ('f, 'a) Logic.datatype list

Sourceval merge : Logic.sort -> Logic.sort -> Logic.sort

Sourceval merge_list : ('a -> Logic.sort) -> Logic.sort -> 'a list -> Logic.sort

Source

val tmap : 
  ('a, 'f) Logic.datatype array ->
  ('a, 'f) Logic.datatype ->
  ('a, 'f) Logic.datatype

Sourceval basename : Logic.sort -> string

Sourceval pretty : Format.formatter -> Logic.sort -> unit

Source

val pp_tau : 
  (Format.formatter -> int -> unit) ->
  (Format.formatter -> 'f -> unit) ->
  (Format.formatter -> 'a -> unit) ->
  Format.formatter ->
  ('f, 'a) Logic.datatype ->
  unit

Source

val pp_data : 
  (Format.formatter -> 'a -> unit) ->
  (Format.formatter -> 'b -> unit) ->
  Format.formatter ->
  'a ->
  'b list ->
  unit

Source

val pp_record : 
  (Format.formatter -> 'f -> unit) ->
  (Format.formatter -> 'b -> unit) ->
  Format.formatter ->
  ?opened:bool ->
  ('f * 'b) list ->
  unit

Source

val eq_tau : 
  ('f -> 'f -> bool) ->
  ('a -> 'a -> bool) ->
  ('f, 'a) Logic.datatype ->
  ('f, 'a) Logic.datatype ->
  bool

Source

val compare_tau : 
  ('f -> 'f -> int) ->
  ('a -> 'a -> int) ->
  ('f, 'a) Logic.datatype ->
  ('f, 'a) Logic.datatype ->
  int

Source

module MakeTau
  (F : Logic.Field)
  (A : Logic.Data) : 
  Logic.Data with type t = (F.t, A.t) Logic.datatype

package frama-c

Module Qed.KindSource

Module `Qed.Kind`Source