daily pastebin goal
65%
SHARE
TWEET

Untitled

a guest Jun 13th, 2018 50 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. module Church where
  2. open import Agda.Primitive
  3.  
  4. Church : {l : Level} -> Set l -> Set l
  5. Church A = (A -> A) -> (A -> A)
  6.  
  7. Nat = {A : Set} -> Church A  
  8. Nat₁ = {A : Set₁} -> Church A
  9. Nat₂ = {A : Set₂} -> Church A
  10.  
  11. c0 : Nat
  12. c0 = s z -> z
  13.  
  14. c1 : Nat
  15. c1 = s z -> s z
  16.  
  17. c2 : Nat
  18. c2 = s z -> s (s z)
  19.  
  20. add : Nat -> Nat -> Nat
  21. add a b s z = b s (a s z)
  22.  
  23. mul : Nat -> Nat -> Nat
  24. mul a b s z = b (a s) z
  25.  
  26. -- First signs of the type growing:
  27. -- exp : {A : Set} -> Church A -> Church (A -> A) -> Church A
  28. exp : Nat -> Nat -> Nat
  29. exp a b = b a
  30.  
  31. tetr : Nat -> Nat₁ -> Nat
  32. tetr k n = n (exp k) c1
  33.  
  34. pent : Nat -> Nat₁ -> Nat
  35. pent k n = n (tetr k) c1 -- error
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top