I have some terms like this:

```
{P : Fin.t n -> Type}
{Q : (forall x, P x) -> Type}
(f : forall (x : forall (y : Fin.t n), P y), Q x)
```

I want to treat `f`

like a function which takes multiple arguments. For this I need to define some sort of `app`

but it is pretty tricky to write down. I would like to be able to write `app f a b c`

which would be translated to `f g`

where `g`

maps each element of `Fin.t 3`

to `a`

, `b`

and `c`

respectively.

It seems the target type of `f`

should depend on the `n`

, and I guess for `n = 0`

we should just return `Q (Fin.case0 P)`

. Not sure how to write down the successor case however. It would need to be `P Fin.F1 -> _`

or something.

And that's just the type of app....

why not write something like

```
Notation "[ x ; y ; .. ; z ]" := (some stuff to build the Fin.t with x y z) : list_scope.
```

and then `f [a;b;c]`

?

seems easier than trying to make application syntax work

Ah ok that seems easier

I've tried something like this but Coq isn't happy with it:

```
Notation "[ x ; y ; .. ; z ]" :=
(fun n =>
match n with
| Fin.F1 => x
| Fin.FS n =>
match n with
| Fin.F1 => y
| Fin.FS n => ..
z
..
end
end).
```

Alright got this to work:

```
Notation "[ x ; y ; .. ; w ; z ]" :=
(fun n =>
match n with
| Fin.F1 => x
| Fin.FS n =>
match n with
| Fin.F1 => y
| Fin.FS n => ..
match n with
| Fin.F1 => w
| Fin.FS n => z
end
..
end
end).
```

Thanks!

I would have considered some `(fun i : Fin.t n => vector_lookup <build vector with a, b, c> i)`

(which I’ve only eta-expanded for clarity)

for a suitable `vector_lookup : Vector.t A n -> Fin.t n -> A`

— I forget the right name (`Vector.lookup`

?)

your notation produces an inlined version and it’s fine, but I’d be worried it’d be harder/slower to reason about

It's called `nth`

.

But that seems to be exactly what I am looking for. Thanks!

Last updated: Jun 18 2024 at 08:01 UTC