bitarrayconvoy.v

Inductive bitarray : nat -> Type :=
| empty : bitarray O
| cons  : forall (sz : nat), bool -> bitarray sz -> bitarray (S sz)
.
 
Notation "{| |}" := empty.
Notation "{| x |}" := (cons _ x empty).
Notation "{| x ; y ; .. ; z |}" := (cons _ x (cons _ y .. (cons _ z empty) .. )).
 
Check {| true; true; false |}.
 
Definition map2 : forall { n : nat }, (bool -> bool -> bool) -> bitarray n -> bitarray n -> bitarray n :=
fix map2_fix { n : nat } f (l : bitarray n) : bitarray n -> bitarray n :=
match l with
| empty => fun r => empty
| @cons n x l' => fun (r : bitarray (S n)) =>
  match r in bitarray (S n) return match (S n) with O => True | S _ => (bitarray n -> bitarray n) -> bitarray (S n) end with
  | cons _ y r' => fun mapfl => @cons _ (f x y) (mapfl r')
  | @empty => I
  end (map2_fix f l')
end.