HyPre.util.VectorPred

From HyPre Require Export
  VectorExtra
  VectorList.

Import VectorListNotations.

Definition v2 {X Y : Type} (P : X -> X -> Y) (xt : Vector.t X 2) : Y
  := P (Vector.nth xt (Fin.F1)) (Vector.nth xt (Fin.FS (Fin.F1))).

Definition vl_hd_P {X : Type} (P : X -> X -> Prop) (xt : Vector.t (list X) 2) : Prop
  := v2 (fun x1 x2 => match x1,x2 with
                   | Some x1, Some x2 => P x1 x2
                   | _,_ => True
                   end) (Vector.map (@hd_error _) xt).