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.

389710 (1) [Avatar] Offline
#1
There is a typo in the predicate `Last` which makes the definition impossible to complete.

The type of the `LastOne` constructor should be `LastOne [value] value`, otherwise pattern matching on the constructor causes
no refinement and makes it impossible to discharge the necessary proof obligations.
Edwin Brady (66) [Avatar] Offline
#2
So it is, thanks for noticing! I've fixed it for the next version.