def Nat : *
let Zero : Nat
let Succ : Nat → Nat
end

def plus : Nat → Nat → Nat
let plus x Zero := x
let plus x (Succ pred) := Succ (plus x pred)
end

def induction : <p[Nat] : *> → p[Zero] → ((pred : Nat) → p[pred] → p[Succ pred]) → ((n : Nat) → p[n])
let induction <p> base step := go
___ def go : (n : Nat) → p[n]
___ let go Zero := base
___ let go (Succ pred) := step pred (go pred)
___ end
end

def hello_world : (n : Nat) → plus Zero n = n
???
end

=가 특별한 built-in type이라고 합시다.
???에 뭐가 들어가야 할까요?
또 증명 시스템은 어떻게 이루어져야 할까요?
이런 체계를 만들어 보고 싶었습니다.

- dc official App