# Commit 2024-10-31 00:24 4b5f1a09

View on Github →feat(Data/Fin/Tuple): Define `Fin.take`

and initial theorems (#17196)
This PR defines `Fin.take`

, which takes the first `m`

elements of an `n`

-tuple (from the left). It requires that `m ≤ n`

, and returns an `m`

-tuple. This is an analogue of `List.take`

.
It also provides initial theorems for `Fin.take`

. If all goes well, I plan to add more theorems over time, and also define `rtake`

to be taking from the right, similar to `List.rtake`

.
Context: I'm working on a formalization of interactive proof systems. As part of that process, I need to define the type of message sent in each round, as something like:

```
def MessageType (numRounds : ℕ) := Fin numRounds → Type
def message (numRounds : ℕ) : ∀ i, (MessageType numRounds) i
```

Then I will also need to talk about composition and restriction of interactive protocols. Composition amounts to `Fin.addCases`

, but restriction is my new `Fin.take`

, and also `Fin.rtake`

in the future (taking from the right).