Hello -- I am trying to write a type for my own copy of `ind-Nat`

in `pie`

, following the example from the original `pie`

documentation. Which states:

```
(ind-Nat target motive base step) → (motive target)
target : Nat
motive : (-> Nat U)
base : (motive zero)
step : (Π ((n Nat))
(-> (motive n)
(motive (add1 n))))
```

This does not survive a copy-paste into racket's interpreter for reasons I shall not go into.

My best attempt to "make it real," so far, has been:

```
(claim iN (Π ((E U))
(→ Nat ; target
(→ Nat U) ; mot, m
E ; base, (m 0)
(→ Nat E E) ; step
E))) ; result, (m ℓ)
(define iN
(λ (E)
(λ (t m b s)
(ind-Nat
t
m
b
s))))
```

which produces an error:

```
; Expected
; (m 0)
; but given E
; Source locations: (the line with b, the base, on it)
```

I have tried many permutations of substituting calls of `m`

, with defining `claim`

s for `b`

, and so on, all leading nowhere better. I'd like to note that the book, "The Little Typer," which has nice descriptions of all this, does *not* exhibit a type for `ind-Nat`

, leading me to suspect:

Is this one of those types that is "expressible but not denotable" in the type-system of `pie`

? Should I give up trying to divinate a type for (my copy of) `ind-Nat`

?