List から Vector を作成したときに，長さの部分が自然数になるようにする

えびさんによる例

import Lean

universe u

inductive Vector (α : Type u) : Nat → Type u where
  | nil : Vector α 0
  | cons : α → {n : Nat} → Vector α n → Vector α (n+1)
deriving Repr

open Lean Meta Elab Term Tactic PrettyPrinter

-- ゴールが`m = rhs`で`m`がメタ変数の時、rhsをwhnfまで簡約した値をmにアサインする
-- アサインした後は`decide`タクティクで証明を試みる
elab "infer_size" : tactic => do
  liftMetaTactic fun goal => do
    goal.checkNotAssigned `infer_size
    goal.withContext do
      let target ← goal.getType
      if let some (_, lhs, rhs) := target.eq? then do
        let calculated ← whnf rhs
        if let false ← isDefEq lhs calculated then
          throwTacticEx `infer_size goal "エラー: lhs と rhs の isDefEqで失敗"

        let proof ← Meta.mkDecideProof target
        if ← isDefEq (mkMVar goal) proof then
          goal.assign proof
          return []
        throwTacticEx `infer_size goal "エラー: decideによる証明失敗"
      else
        throwTacticEx `infer_size goal "エラー: ゴールがEqじゃなかった。ゴールが?m = e でeが変数を含まない自然数の足し算であることを期待している"

def Vector.cons'
  {α : Type} (a : α) {n : Nat} (as : Vector α n)
  {m : Nat} (h : m = n + 1 := by infer_size)
  : Vector α m := by rw [h]; exact Vector.cons a as

syntax (name := vectorLit) "![" term,* "]" : term

partial def toVecConsStx : TSyntaxArray `term → TermElabM (TSyntax `term) := fun arr =>
  if arr.size = 0
    then `(Vector.nil)
    else do
      let a := arr.get! 0
      let as ← toVecConsStx <| arr.reverse.pop.reverse
      `(Vector.cons' $a $as)

@[term_elab vectorLit]
def vectorLitImpl : TermElab := fun stx typ? => do
  let args := TSyntaxArray.mk stx[1].getSepArgs
  let stx ← toVecConsStx args
  elabTerm stx typ?

@[app_unexpander Vector.nil]
def unexpandVecNil : Unexpander
  | `(Vector.nil) => `(![])
  | _ => throw ()
def unexpandVecCons : Unexpander
  | `(Vector.cons' $a:term ![] $_) => `(![$a])
  | `(Vector.cons' $a:term ![$as:term,*] $_) => `(![$a, $as,*])
  | _ => throw ()
attribute [app_unexpander Vector.cons'] unexpandVecCons

#check ![]
#check ![1]
#check ![1, 2]
#eval ![1, 2]

#check_failure (![1] : Vector Nat 0)

The issue only provides an inline Lean example defining Vector and its syntax elaborator; it names no repository file, test, or existing List conversion entry point. First clarify where this example belongs and the intended behavior, then define completion criteria for producing a Vector whose length is a natural number.