1
$\begingroup$

I am defining the type Nat of natural numbers a recursive sum type:

$$ Nat = \mu X. Unit \oplus X$$

Now, I have defined zero as the term:

zero : Nat
zero = fold Nat (Inl tmUnit tyNat tyUnit)

and successor as

succ : Nat -> Nat
succ n = fold Nat (tmInr n tyNat tyUnit)

Please note, that I am not completely sure of these two implementations; they might be wrong - I accept comments on them too.

Now, my question: I want to implement a predecessor function. I have both an isZero function and an if-then-else construct. How could I to this?

Improve this question
$\endgroup$
2
  • $\begingroup$ I'll assume you're trying to study type encodings. Could you please show a more complete source of what you have so far? For example, your definitions of Nat, and isZero. $\endgroup$
    – paulotorrens
    Commented Dec 19, 2019 at 21:39
  • $\begingroup$ I am not well versed with Agda, but will copying church encoding for predecessor help in your case? en.wikipedia.org/wiki/… $\endgroup$
    – Apoorv
    Commented Jan 9, 2020 at 17:13

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.