Commit 9cc138e4 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Improve boxing of tuples in Coq printer.

parent 94ff3db7
......@@ -19,12 +19,12 @@ Require list.List.
(* combine is replaced with (Lists.List.combine x x1) by the coq driver *)
(* Why3 goal *)
Lemma combine_def : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (x:(list a)) (y:(list b)), match (x,
y) with
Lemma combine_def :
forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (x:(list a)) (y:(list b)),
match (x, y) with
| ((Init.Datatypes.cons x0 x1), (Init.Datatypes.cons y0 y1)) =>
((Lists.List.combine x y) = (Init.Datatypes.cons (x0,
y0) (Lists.List.combine x1 y1)))
((Lists.List.combine x y) = (Init.Datatypes.cons (x0, y0) (Lists.List.combine x1 y1)))
| _ => ((Lists.List.combine x y) = Init.Datatypes.nil)
end.
Proof.
......
......@@ -183,16 +183,10 @@ let unambig_fs fs =
(** Patterns, terms, and formulas *)
(* unused
let lparen_l fmt () = fprintf fmt "@ ("
*)
let lparen_r fmt () = fprintf fmt "(@,"
(* unused
let print_paren_l fmt x =
print_list_delim ~start:lparen_l ~stop:rparen ~sep:comma fmt x
*)
let lparen_r fmt () = fprintf fmt "@[<hov 1>("
let rparen_r fmt () = fprintf fmt ")@]"
let print_paren_r fmt x =
print_list_delim ~start:lparen_r ~stop:rparen ~sep:comma fmt x
print_list_delim ~start:lparen_r ~stop:rparen_r ~sep:comma fmt x
let arrow fmt () = fprintf fmt " ->@ "
let print_arrow_list fmt x = print_list_suf arrow fmt x
......
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