package why3find

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Why3find.Session`Source

Sourcetype session

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

Sourceval save : session -> unit

Sourcetype theory

Sourceval name : theory -> string

Sourceval theory : theory -> Why3.Theory.theory

Sourceval theories : session -> theory list

Sourcetype goal

Sourceval split : theory -> goal list

Sourceval goal_name : goal -> string

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

Sourceval goal_task : goal -> Why3.Task.task

Sourceval goal_expl : goal -> string

Sourceval goal_idename : goal -> string

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

Sourceval thy_name : Why3.Theory.theory -> string

Sourceval proof_name : Why3.Ident.ident -> string

Sourceval task_name : Why3.Task.task -> string

Sourceval task_expl : Why3.Task.task -> string

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

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