aux_decl_zeta.lean:11:48: error: equation compiler failed to create auxiliary declaration 'f._match_1', auxiliary declaration has references to let-declarations (possible solution: use 'set_option eqn_compiler.zeta true')
nested exception message:
type mismatch at application
  x = w
term
  w
has type
  vec ℕ n
but is expected to have type
  vec ℕ 10
aux_decl_zeta.lean:5:11: warning: declaration 'f' uses sorry
