Commit b89ed0ef authored by Guillaume Melquiond's avatar Guillaume Melquiond

Improve inductive predicates in Coq printer.

parent 81b34ace
......@@ -22,10 +22,11 @@ Require list.Append.
(* Why3 assumption *)
Inductive distinct {a:Type} {a_WT:WhyType a}: (list a) -> Prop :=
| distinct_zero : distinct Init.Datatypes.nil
| distinct_one : forall (x:a), (distinct
(Init.Datatypes.cons x Init.Datatypes.nil))
| distinct_many : forall (x:a) (l:(list a)), (~ (list.Mem.mem x l)) ->
((distinct l) -> (distinct (Init.Datatypes.cons x l))).
| distinct_one :
forall (x:a), distinct (Init.Datatypes.cons x Init.Datatypes.nil)
| distinct_many :
forall (x:a) (l:(list a)), ~ (list.Mem.mem x l) -> (distinct l) ->
distinct (Init.Datatypes.cons x l).
(* Why3 goal *)
Lemma distinct_append {a:Type} {a_WT:WhyType a} :
......
......@@ -821,7 +821,7 @@ let print_recursive_decl ~old info fmt dl =
List.iter (print_equivalence_lemma ~old info fmt) dl_syn
let print_ind info fmt (pr,f) =
fprintf fmt "@[<4>| %a : %a@]" print_pr pr (print_term info) f
fprintf fmt "@[<hv 4>| %a :@ @[%a@]@]" print_pr pr (print_term info) f
let print_ind_decl info fmt ps bl =
let _, _, all_ty_params = ls_ty_vars ps in
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment