1. Lab 01: Setup (30/1/2023).
  2. Lab02: Selection Sort (part 1) and `≤` on `Answer` (6/2/2023).
  3. Lab03 Selection Sort (part 2) (13/2/2023).
  4. Vectors: Equivalence of definitions (20/3/2023).

Vectors: Equivalence of definitions

due by Monday, Mar 20, 2023

Before doing this assignment you will need to pull from the upstream repository, i.e., the course repository. Please complete the definitions/proofs in the file PnP2023/Labs/Lab04/VecVector.lean. When you are done please commit and push your changes to your forked private repository and alert me on Zulip.

  1. Complete the definition of Vec.ofVector.

  2. Complete the definition of Vec.toVector.

  3. Complete the proof of Vec.ofVector.toVector.

  4. Complete the proof of Vec.toVector.ofVector.