Commit 42da66bf authored by Robbert Krebbers's avatar Robbert Krebbers

Add `TCForall2`.

parent e8d81825
Pipeline #5798 passed with stages
in 7 minutes and 37 seconds
......@@ -91,6 +91,14 @@ Existing Class TCForall.
Existing Instance TCForall_nil.
Existing Instance TCForall_cons.
Inductive TCForall2 {A B} (P : A B Prop) : list A list B Prop :=
| TCForall2_nil : TCForall2 P [] []
| TCForall2_cons x y xs ys :
P x y TCForall2 P xs ys TCForall2 P (x :: xs) (y :: ys).
Existing Class TCForall2.
Existing Instance TCForall2_nil.
Existing Instance TCForall2_cons.
(** Throughout this development we use [stdpp_scope] for all general purpose
notations that do not belong to a more specific scope. *)
Delimit Scope stdpp_scope with stdpp.
......
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