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.

392661 (2) [Avatar] Offline
#1
Hi Everyone,

I'm not sure to get the idea behind the "impossible" keyword.
Is it an optional keyword (only for readability purposes) or are there any cases where it matters to the coverage checker (in terms of either performance or correctness)?

Cheers,
392661 (2) [Avatar] Offline
#2
- Another related question is about the following example In page 278

twoPlusTwoNotFive : 2 + 2 = 5 -> Void
twoPlusTwoNotFive Refl impossible

I wonder if that means that if we replace 2 + 2 = 5 by any false hypothesis (over Nat) then the compiler will be able to decide in a general way if it's indeed false by typechecking (or refusing to) the following
FalseHypothesis NatEqProposition -> Void
FalseHypothesis Refl impossible

and if it generalizes to equality propositions over other data types (involving total functions)?