Module Rtauto_plugin.Proof_searchSource

Sourcetype form =
  1. | Atom of int
  2. | Arrow of form * form
  3. | Bot
  4. | Conjunct of form * form
  5. | Disjunct of form * form
Sourcetype proof =
  1. | Ax of int
  2. | I_Arrow of proof
  3. | E_Arrow of int * int * proof
  4. | D_Arrow of int * proof * proof
  5. | E_False of int
  6. | I_And of proof * proof
  7. | E_And of int * proof
  8. | D_And of int * proof
  9. | I_Or_l of proof
  10. | I_Or_r of proof
  11. | E_Or of int * proof * proof
  12. | D_Or of int * proof
  13. | Pop of int * proof
Sourcetype state
Sourceval project : state -> proof
Sourceval init_state : ('a * form * 'b) list -> form -> state
Sourceval branching : state -> state list
Sourceval success : state -> bool
Sourceval pp : state -> Pp.t
Sourceval pr_form : form -> Pp.t
Sourceval reset_info : unit -> unit
Sourceval pp_info : unit -> unit