The Little Typer Exercise 3.4

Exercise 3.4.rkt

#lang pie

(claim >
  (-> Nat Nat Nat))
(define >
  (lambda (n)
    (rec-Nat n
      (the (-> Nat Nat) (lambda (m) 0))
      (lambda (n-1 n-1>)
        (lambda (m)
          (rec-Nat m
            1
            (lambda (m-1 _)
              (n-1> m-1))))))))

(claim max
  (-> Nat Nat Nat))
(define max
  (lambda (n m)
    (rec-Nat (> n m)
      m
      (lambda (_ _) n))))

(check-same Nat 0 (max 0 0))
(check-same Nat 1 (max 1 0))
(check-same Nat 1 (max 0 1))
(check-same Nat 2 (max 2 1))
(check-same Nat 2 (max 1 2))

I would be, but unfortunately I am not — I’m in NYC.

…

On Mon, Feb 3, 2020 at 7:48 AM aymanosman ***@***.***> wrote: Thanks for the pointers. You may be interested in this group https://www.meetup.com/London-TyDD, if you are based in London. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <https://gist.github.com/9db1db11755ef4b4759c4ee9a4bdb515?email_source=notifications&email_token=AAABM3JIFCKQI2R7VTD5CXTRBAHBPA5CNFSM4KLSD4OKYY3PNVWWK3TUL52HS4DFVNDWS43UINXW23LFNZ2KUY3PNVWWK3TUL5UWJTQAGBFAC#gistcomment-3164673>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAABM3KLL6CMNI427F3ZRRDRBAHBPANCNFSM4KLSD4OA> .