package why3find

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

type t = Why3.Ident.ident

val hash : t -> int

val equal : t -> t -> bool

val compare : t -> t -> int

val pp : Format.formatter -> t -> unit

val ppr : Format.formatter -> t -> unit

val loc : t -> Why3.Loc.position

val file : t -> string

val line : t -> int

val path : ?lib:string list -> t -> string list * string * string list

val fullname : ?lib:string list -> t -> string

val cat : string list -> string

type package = [

]

type id = {

}

val lemma : t -> bool

val standard : t -> bool

val resolve : lib:string list -> ?root:string -> t -> id

val of_infix : string -> string

val to_infix : string -> string

val pp_path : Format.formatter -> (string list * string * string list) -> unit

val pp_qid : Format.formatter -> string list -> unit

val pp_qpath : local:string list -> Format.formatter -> id -> unit

only the prefix path of qid after local

val pp_qname : Format.formatter -> id -> unit

only the (infix) name of qid

val name : id -> string

only the last (infix) part of qid

val pp_local : Format.formatter -> id -> unit

only the qualified name (qid)

val pp_title : Format.formatter -> id -> unit

the full path name

val pp_aname : Format.formatter -> id -> unit

val pp_ahref : 
  current:string option ->
  package_url:string option ->
  Format.formatter ->
  id ->
  unit

val pp_proof_aname : Format.formatter -> id -> unit

val pp_proof_ahref : Format.formatter -> id -> unit

type decl =

val find : Why3.Theory.theory -> t -> decl