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 session

val create : 
  session:bool ->
  dir:string ->
  file:string ->
  format:string ->
  Why3.Theory.theory list ->
  session

val save : session -> unit

type theory

val name : theory -> string

val theory : theory -> Why3.Theory.theory

val theories : session -> theory list

type goal

val split : theory -> goal list

val goal_name : goal -> string

val goal_loc : goal -> Why3.Loc.position option

val goal_task : goal -> Why3.Task.task

val goal_expl : goal -> string

val goal_idename : goal -> string

val pp_goal : Format.formatter -> goal -> unit

val thy_name : Why3.Theory.theory -> string

val proof_name : Why3.Ident.ident -> string

val task_name : Why3.Task.task -> string

val task_expl : Why3.Task.task -> string

val result : 
  goal ->
  Why3.Whyconf.prover ->
  Why3.Call_provers.resource_limits ->
  Why3.Call_provers.prover_result ->
  unit

val apply : Why3.Env.env -> Tactic.tactic -> goal -> goal list option