Unknown variable +

Question

In the Little Typer chapter 2 frame 100 gives the following definition:

(claim pearwise+
  (→ Pear Pear
     Pear))

(define pearwise+
  (λ (anjou bosc)
    (elim-Pear anjou
      (λ (a1 d1)
        (elim-Pear bosc
          (λ (a2 d2)
            (cons
              (+ a1 a2)
              (+ d1 d2))))))))

When I run it I get the following error:

Unknown variable +

What is wrong?

Answer 1

Pie does not ship out of the box with an addition function but chapter 3 frames 24, 26, and 27 of the Little Typer give the following definition for +:

; 3.26
(claim step-+
  (→ Nat
      Nat))

(define step-+
  (λ (+n-1)
    (add1 +n-1)))

; 3.24
(claim +
  (→ Nat Nat
      Nat))

; 3.27
(define +
  (λ (n j)
    (iter-Nat n
      j
      step-+)))

Put these before the definition of pairwise+ to use + in the definition.

The complete solution would look like this:

#lang pie

; 2.80
(claim Pear U)

(define Pear
  (Pair Nat Nat))

; 2.82
(check-same Pear (cons 3 5) (cons 3 (add1 4)))

; 2.93
(claim Pear-maker U)

(define Pear-maker
  (→ Nat Nat
      Pear))

(claim elim-Pear
  (→ Pear Pear-maker
      Pear))

(define elim-Pear
  (λ (pear maker)
    (maker (car pear) (cdr pear))))

; 2.95
(check-same (Pair Nat Nat)
  (cons 17 3)
  (elim-Pear
    (cons 3 17)
    (λ (a d)
      (cons d a))))

;----------------------
; need to add + define
; taken from chapter 3
;----------------------

; 3.26
(claim step-+
  (→ Nat
      Nat))

(define step-+
  (λ (+n-1)
    (add1 +n-1)))

; 3.24
(claim +
  (→ Nat Nat
      Nat))

; 3.27
(define +
  (λ (n j)
    (iter-Nat n
      j
      step-+)))

; 2.100
(claim pearwise+
  (→ Pear Pear
     Pear))

(define pearwise+
  (λ (anjou bosc)
    (elim-Pear anjou
      (λ (a1 d1)
        (elim-Pear bosc
          (λ (a2 d2)
            (cons
              (+ a1 a2)
              (+ d1 d2))))))))

(check-same Pear
  (cons 3 4)
  (pearwise+
    (cons 1 2)
    (cons 2 2)))