helm/ocaml/tactics/tactics.mli

   1 (* GENERATED FILE, DO NOT EDIT *)
   2 val absurd : term:Cic.term -> ProofEngineTypes.tactic
   3 val apply : term:Cic.term -> ProofEngineTypes.tactic
   4 val assumption : ProofEngineTypes.tactic
   5 val auto : ?num:int option -> Mysql.dbd -> ProofEngineTypes.tactic
   6 val auto_new :
   7   ?depth:int ->
   8   ?width:int -> dbd:Mysql.dbd -> unit -> ProofEngineTypes.tactic
   9 val change : what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic
  10 val compare : term:Cic.term -> ProofEngineTypes.tactic
  11 val constructor : n:int -> ProofEngineTypes.tactic
  12 val contradiction : ProofEngineTypes.tactic
  13 val cut :
  14   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
  15   Cic.term -> ProofEngineTypes.tactic
  16 val decide_equality : ProofEngineTypes.tactic
  17 val decompose :
  18   ?uris_choice_callback:((UriManager.uri * int *
  19                           (UriManager.uri * Cic.term) list)
  20                          list ->
  21                          (UriManager.uri * int *
  22                           (UriManager.uri * Cic.term) list)
  23                          list) ->
  24   Cic.term -> ProofEngineTypes.tactic
  25 val discriminate : term:Cic.term -> ProofEngineTypes.tactic
  26 val elim_intros_simpl : term:Cic.term -> ProofEngineTypes.tactic
  27 val elim_intros : term:Cic.term -> ProofEngineTypes.tactic
  28 val elim_type : term:Cic.term -> ProofEngineTypes.tactic
  29 val exact : term:Cic.term -> ProofEngineTypes.tactic
  30 val exists : ProofEngineTypes.tactic
  31 val fold :
  32   reduction:(Cic.context -> Cic.term -> Cic.term) ->
  33   also_in_hypotheses:bool -> term:Cic.term -> ProofEngineTypes.tactic
  34 val fourier : ProofEngineTypes.tactic
  35 val generalize :
  36   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
  37   term:Cic.term -> ProofEngineTypes.pattern -> ProofEngineTypes.tactic
  38 val set_goal : int -> ProofEngineTypes.tactic
  39 val injection : term:Cic.term -> ProofEngineTypes.tactic
  40 val intros :
  41   ?howmany:int ->
  42   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
  43   unit -> ProofEngineTypes.tactic
  44 val left : ProofEngineTypes.tactic
  45 val letin :
  46   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
  47   Cic.term -> ProofEngineTypes.tactic
  48 val reduce : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
  49 val reflexivity : ProofEngineTypes.tactic
  50 val replace : what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic
  51 val rewrite_back :
  52   ?where:ProofEngineTypes.pattern ->
  53   term:Cic.term -> unit -> ProofEngineTypes.tactic
  54 val rewrite_back_simpl :
  55   ?where:ProofEngineTypes.pattern ->
  56   term:Cic.term -> unit -> ProofEngineTypes.tactic
  57 val rewrite :
  58   ?where:ProofEngineTypes.pattern ->
  59   term:Cic.term -> unit -> ProofEngineTypes.tactic
  60 val rewrite_simpl :
  61   ?where:ProofEngineTypes.pattern ->
  62   term:Cic.term -> unit -> ProofEngineTypes.tactic
  63 val right : ProofEngineTypes.tactic
  64 val ring : ProofEngineTypes.tactic
  65 val simpl : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
  66 val split : ProofEngineTypes.tactic
  67 val symmetry : ProofEngineTypes.tactic
  68 val transitivity : term:Cic.term -> ProofEngineTypes.tactic
  69 val whd : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
  70 val normalize : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
  71 val fwd_simpl : hyp:Cic.name -> dbd:Mysql.dbd -> ProofEngineTypes.tactic
  72 val lapply :
  73   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
  74   ?substs:(Cic.name * Cic.term) list -> Cic.term -> ProofEngineTypes.tactic