Andreas Reuleaux (7) [Avatar] Offline
A minor thing, but nevertheless: In the course of developing checkEqNat in the Type/Define/Refine style

in step 6 (Define) Just eq is introduced (instead of Just x):

...We'll rename the Just x produced by the case split to something
more informative, and fill in the case where the recursive call
produces Nothing:

 checkEqNat (S k) (S j) = case checkEqNat k j of
                               Nothing => Nothing
                               Just eq => ?checkEqNat_rhs_2

Just eq is also used in step 8 (Refine, page 249), and step 9 (Refine, p 249)

Consequently when I work through the example and
look at the type of ?checkEqNat_rhs_2 in step 7
I get to see eq as well in the premisses:

  k : Nat
  j : Nat
  eq : EqNat k j
Main.checkEqNat_rhs_2 : Maybe (EqNat (S k) (S j))

ie. eq, not rec_eq as is currently printed for step 7 in the book:

  k : Nat
  j : Nat
  rec_eq : EqNat k j
checkEqNat_rhs_2 : Maybe (EqNat (S k) (S j))

Edwin Brady (65) [Avatar] Offline
Thanks! I have presumably renamed this at some stage and missed an occurrence. It'll be fixed soon.