Mentions légales du service

Skip to content
Snippets Groups Projects
Commit 61e9eb85 authored by BERTOT Yves's avatar BERTOT Yves
Browse files

remove the last definition that is problematic

parent 4889aeef
No related branches found
No related tags found
No related merge requests found
...@@ -99,10 +99,3 @@ apply (redo_rev_tree_elim (fun t x => x = rev_tree t)). ...@@ -99,10 +99,3 @@ apply (redo_rev_tree_elim (fun t x => x = rev_tree t)).
intros a t1 t2 IH1 IH2; simpl; rewrite IH1, IH2. intros a t1 t2 IH1 IH2; simpl; rewrite IH1, IH2.
easy. easy.
Qed. Qed.
Equations redo_rev_tree' {T} (t : btree T) : btree T :=
redo_rev_tree' t by rec t (@ltt T) :=
redo_rev_tree' Leaf := Leaf ;
redo_rev_tree' (Node a t1 t2) := Node a (redo_rev_tree t2)
(redo_rev_tree t1).
.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment