在 pie-lang 中为 which-Nat 写一个类型

Question

阅读后which-Nat的文档，复制在这里：

(which-Nat target base step) → X

      target : Nat
      base : X
      step : (-> Nat X)

which-Nat is a case operator on Nat.

Examples:

    > (which-Nat 0 0 (λ (smaller) smaller))

    (the Nat 0)
    > (which-Nat 17 0 (λ (smaller) smaller))

    (the Nat 16)

我试着写我自己的克隆，

wN

，但是下面的声明

(claim wN
       (Π ((E      U        )
           (target Nat      )
           (base   E        )
           (step   (→ Nat E)))
          (→ target base step
             E)))

产生错误

; Expected U but given Nat 

修复完全不能令人满意：

(claim wN
       (Π ((E      U        )
           (target Nat      )
           (base   E        )
           (step   (→ Nat E)))
          (→ U U U ;target base step
             E)))

所有三个

U

都是强制的，因为如果使用

target

，

base

和

step

中的任何一个，我都会遇到同样的失败。

这更令人惊讶，因为我克隆了更具挑战性的

ind-Nat

，即

iN

，通过其文档的类似转录，作品：

(claim iN
       (Π ((t   Nat)                    ; target
           (m   (→ Nat U))              ; motive
           (b   (m 0))                  ; base
           (s   (Π ((n-1 Nat))          ; step
                   (→ (m n-1)
                      (m (add1 n-1))))))
          (m t)))

(define iN
  (λ (t m b s)
    (ind-Nat
     t
     m
     b
     s)))

;; unit tests

(claim peas-ex
       (Π ((ℓ Nat))
          (Vec Atom ℓ)))

(define peas-ex
  (λ (ℓ)
    (iN ℓ
        mot-peas
        base-peas
        step-peas)))

(peas-ex 0)
(peas-ex 1)
(peas-ex 2)

which-Nat

的最具体和正确的类型是什么，它可以让我

define

像我为

ind-Nat

所做的那样克隆？