NuPRL 中的证明(Leftpad)
本次要用 CTT 来写 Leftpad1，以说明即使不能实际运行 NuPRL 仍是个很好的 programming logic？(因为如下证明我是直接写的，没在 NuPRL 里跑) Takes a padding character, a string, and a total length, returns the string padded to that length with that character. If length is less than the length of the string, does nothing. 问題到手，首先定义的是 string 的 axioms $$\forall x: \mathbb{N}. Str(x) \in Type\\C \in Type\\ \forall x: \mathbb{N}, y: \mathbb{N}_x, a : Str(x). a\ !!\ y \in C\\ \forall x: \mathbb{N}, a : Str(x)....