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?

$\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 Dec 19 '19 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 Jan 9 '20 at 17:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.