Error "unknown identifier 'hp'" in chapter 3 "Propositions and Proofs" when using `variable (hp: p)`

[MichaelJFishman]

Description

Lean gives the error "unknown identifier 'hp'" when I put this example code into an otherwise empty file:

variable {p q : Prop}
variable (hp : p)

theorem t1 : q → p := fun (hq : q) => hp

Possible solution

The code will type check if I change hp: p to an axiom:

variable {p q : Prop}
axiom hp: p

theorem t1 : q → p := fun (hq : q) => hp

However, #print t1 gives me

∀ {p q : Prop}, q → p := fun {p q} hq => hp

not

∀ p q : Prop, p → q → p

which is what the book states the type should be.

Other things I tried that didn't type check

I tried applying one, the other, or both of the following:

1. Using curly braces variable {hp : p} to make hp get used implicitly.
2. Changing t1 to t1 : p → q → p.

With both applied:

variable {p q : Prop}
variable {hp : p}

theorem t1 : p → q → p := fun (hq : q) => hp

Environment

Lean (version 4.12.0, x86_64-unknown-linux-gnu, commit dc2533473114, Release)

Edit: Changed #check t1 to #print t1. Edit 2: Added link to book section