package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type form =
  1. | Atom of int
  2. | Arrow of form * form
  3. | Bot
  4. | Conjunct of form * form
  5. | Disjunct of form * form
type 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
type state
val project : state -> proof
val init_state : ('a * form * 'b) list -> form -> state
val branching : state -> state list
val success : state -> bool
val pp : state -> Pp.t
val pr_form : form -> Pp.t
val reset_info : unit -> unit
val pp_info : unit -> unit