summaryrefslogtreecommitdiff
path: root/plugins/funind/functional_principles_types.mli
blob: fb04c6ec28a960f0d7e2b9cb7626c49d54f0c5d6 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
open Names
open Term


val generate_functional_principle :
  (* do we accept interactive proving *)
  bool ->
  (* induction principle on rel *)
  types ->
  (* *)
  sorts array option ->
  (* Name of the new principle *)
  (identifier) option ->
  (* the compute functions to use   *)
  constant array ->
  (* We prove the nth- principle *)
  int  ->
  (* The tactic to use to make the proof w.r
     the number of params
  *)
  (constr array -> int -> Tacmach.tactic) ->
  unit

val compute_new_princ_type_from_rel : constr array -> sorts array ->
  types -> types


exception No_graph_found

val make_scheme : (constant*Rawterm.rawsort) list -> Entries.definition_entry list

val build_scheme : (identifier*Libnames.reference*Rawterm.rawsort) list ->  unit
val build_case_scheme : (identifier*Libnames.reference*Rawterm.rawsort)  ->  unit