The Little Typer

In "The Little Typer" book, I am just starting to use DrRacket. From a David Christiansen video, I inputted:

(claim two-plus-two-is-four
  (= Nat (+ 2 2) 4))

which returned an error:

 claim : this function is not defined.

Why?

Solution

First you need to install pie. In DrRacket you can do this with: File > Package Manager... > Do What I Mean, typing pie in the package source field, and clicking Install.

Alternatively, if you're using the command line you can install it with the command:

raco pkg install pie

Second, if you're using DrRacket you need to make sure "Determine Language from Source" is selected at the bottom-left of the window (on the command-line this is the default).

Third, put #lang pie at the top of your file.

#lang pie

(claim two-plus-two-is-four
  (= Nat (+ 2 2) 4))

This still doesn't work because + isn't built-in; it can be defined in terms of other things that are built-in (this is discussed on pages 72 - 77 of the book).