The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

I was playing a little bit with predicative Church numerals

Definition nat := forall X : Type, (X -> X) -> X -> X.

Some functions are easy to define...

Definition plus (n m : nat) : nat :=

  fun X f x => n X f (m X f x).

Definition mult (n m : nat) : nat :=

  fun X f x => n X (m X f) x.

Definition exp (n m : nat) : nat :=

  fun X f x => m (X -> X) (n X) f x.

... However, when trying to go one level up and code a tower of exponentials, I got stuck. Can it be done at all with a predicative encoding?

--
Arthur Azevedo de Amorim