Module `Why3find.Id`Source

Sourcetype t = Why3.Ident.ident

Sourceval hash : t -> int

Sourceval equal : t -> t -> bool

Sourceval compare : t -> t -> int

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

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

Sourceval loc : t -> Why3.Loc.position

Sourceval file : t -> string

Sourceval line : t -> int

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

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

Sourceval cat : string list -> string

Sourcetype package = [

]

Sourcetype id = {

}

Sourceval lemma : t -> bool

Sourceval standard : t -> bool

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

Sourceval of_infix : string -> string

Sourceval to_infix : string -> string

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

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

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

only the prefix path of qid after local

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

only the (infix) name of qid

Sourceval name : id -> string

only the last (infix) part of qid

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

only the qualified name (qid)

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

the full path name

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

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

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

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

Sourcetype decl =

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

package why3find