The Author Online Book Forums are Moving

The Author Online Book Forums will soon redirect to Manning's liveBook and liveVideo. All book forum content will migrate to liveBook's discussion forum and all video forum content will migrate to liveVideo. Log in to liveBook or liveVideo with your Manning credentials to join the discussion!

Thank you for your engagement in the AoF over the years! We look forward to offering you a more enhanced forum experience.

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 (66) [Avatar] Offline
Thanks! I have presumably renamed this at some stage and missed an occurrence. It'll be fixed soon.