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