Currently language-pts doesn't allow extending the system. (There are commented out "hardcoded" snippets though).

Yet, we can add types to the context (natCtx) and typeCheck the plus function.

>>> prettyPut $ natCtx @LambdaStar "succ"
Nat → Nat

>>> prettyPut $ natCtx @LambdaStar "natElim"
∏ (m : (Nat → ⋆)) →
m zero →
(∏ (l : Nat) → m l → m (succ l)) →
∏ (k : Nat) →
m k

But if we try to evaluate plus, we are stuck:

>>> demo_ natCtx $ lambdaStarPlus @@ ("succ" @@ "zero") @@ "zero"
natElim (λ _ → Nat → Nat)
        (λ n → n)
        (λ k rec n → succ (rec n))
        (succ zero)
        zero
    ↪ natElim (λ _ → Nat → Nat)
              (λ n → n)
              (λ k rec n → succ (rec n))
              (succ zero)
              zero
    : Nat

This is small script to test dumpDefs_ implementation.

>>> runLoud $ spec_ (MartinLof 0) >> natScript
λ» :define Nat = ℕ
λ» :define zero = 0
λ» :define succ : Nat → Nat = λ n → S n
λ» :define 0 = zero
λ» :define 1 = succ 0
λ» :define 2 = succ 1
Nat = ℕ
zero = 0
succ = λ n → S n : Nat → Nat
0 = zero
1 = succ 0
2 = succ 1
∎