Type of de Burjin index

好亂,整理成一篇文章好了
順便釐清看看

前言一下
list A ::= [] | list A : a.
且, 用 list 表示 context: Γ.

首先,來看幾個case

λ.0 : [] ; a -> a
λλ.0 : [] ; a -> b -> b
λλ.1 : [] ; a -> b -> a
λλλ.2 : [] ; a -> b -> c -> a

然後根據某條rule

λ_ : Term (G,T) T' -> Term G (T -> T')

就變成了

0 : [a] ; a
λ.0 : [a] ; b -> b
λ.1 : [a] ; b -> a
λλ.2 : [a] ; b -> c -> a

後三個case可以再來一次

0 : [a,b] ; b
1 : [a,b] ; a
λ.2 : [a,b] ; c -> a

最後一個case還可以更進一步

2 : [a,b,c] ; a

結論
確實,不管有幾層λ-binder
如果是取 zero
那就是直接取出context最後進來的
如果是取 suc zero
就是往後數一個
取 suc suc zero
則再往後取一個

--
明白以後..
突然覺得這兩三天的時間...
實在是花得很浪費= =