package why3

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

type engine

type params = {

}

val create : params -> Env.env -> Decl.decl Ident.Mid.t -> engine

exception NotARewriteRule of string

val add_rule : Term.term -> engine -> engine

val normalize : 
  ?step_limit:int ->
  limit:int ->
  engine ->
  Term.term ->
  Term.term

exception NoMatch of (Term.term * Term.term * Term.term option) option

exception NoMatchpat of (Term.pattern * Term.pattern) option

type substitution = Term.term Term.Mvs.t

val first_order_matching : 
  Term.Svs.t ->
  Term.term list ->
  Term.term list ->
  Ty.ty Ty.Mtv.t * substitution