---
tags: violet
---
# Simpler indexed data type

現在只有一些非常簡單的 data type 可以被定義，像是

data Nat
| zero
| suc Nat

data Bool
| true
| false

引入 simpler indexed data type 之後就會有

data Vec (n : Nat) (a : Type)
match n
| zero => nil
| suc n' => cons a (Vec n' a)

這需要更新 `dataTypeCtx` 這個欄位，讓它搜尋時要使用 `.rigid Vec` 的 spine，並對這個 partial pattern 進行 matching 來找到當前能使用的 pattern head