package why3

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

val field : int -> string

val structs : C.struct_def Ident.Hid.t

val aliases : C.ty Ident.Hid.t

val array : Ident.attribute

val array_mk : Ident.attribute

val likely : Ident.attribute

val unlikely : Ident.attribute

val decl_attribute : Ident.attribute

val ty_of_ty : info -> Ty.ty -> C.ty

val ty_of_mlty : info -> Mltree.ty -> C.ty

val struct_of_rs : info -> Expr.Wrs.key -> C.struct_def

val ity_of_expr : Mltree.expr -> Ity.ity

val pv_name : Ity.pvsymbol -> Ident.ident

val is_constructor : Expr.rsymbol -> Pdecl.its_defn -> bool

val is_struct_constructor : info -> Expr.rsymbol -> bool

val struct_of_constructor : info -> Expr.rsymbol -> C.struct_def

type syntax_env = {

}

val is_true : Mltree.expr -> bool

val is_false : Mltree.expr -> bool

val is_unit : Mltree.ity -> bool

val handle_likely : Ident.Sattr.t -> C.expr -> C.expr

val reverse_likely : C.expr -> C.expr

val expr_or_return : syntax_env -> C.expr -> C.stmt

val ity_escapes_from_expr : syntax_env -> Ity.ity -> Mltree.expr -> bool

val var_escapes_from_expr : syntax_env -> Ity.pvsymbol -> Mltree.expr -> bool

val expr : info -> syntax_env -> Mltree.expr -> C.body

val translate_decl : info -> Mltree.decl -> header:bool -> C.definition list