メモ：infer_var

[Seasawher]

SciLean に登場するすごく良いアイデアのひとつ

see: https://lecopivo.github.io/scientific-computing-lean/working-with-arrays/tensor-operations.html#pooling-and-difficulties-with-dependent-types

[Seasawher]

The most flexible way of writing the avgPool function is as follows:

def avgPool (x : Float^[n]) {m} (h : m = n/2 := by infer_var) : Float^[m] :=
  ⊞ (i : Fin m) =>
    let i1 : Fin n := ⟨2*i.1, by omega⟩
    let i2 : Fin n := ⟨2*i.1+1, by omega⟩
    0.5 * (x[i1] + x[i2])