Gokul (Aug 01 2023 at 17:06): Gokul (Aug 01 2023 at 17:06):I have a question, what does "hd []" evaluate to? Actually I am trying to prove something like "x ∉ (hd ([]))"
Wolfgang Jeltsch (Aug 01 2023 at 17:27):The head of the empty list is unspecified. Therefore, you can’t prove anything about it except for things that hold for any value of the respective type. For example, you can prove that hd [] :: bool is either False or True, but you can’t, for example, prove that hd [] :: 'a set is the empty set, because it could be any set.
Gokul (Aug 01 2023 at 17:37):Thanks!
Mathias Fleury (Aug 02 2023 at 19:06):The worst example I ever had was a case where hd [] = hd [] was not provable
Mathias Fleury (Aug 02 2023 at 19:06):this is always true… unless there is some implicit conversion going on
Mathias Fleury (Aug 02 2023 at 19:07):hd ([]::real list) = hd ([] :: nat list)
Wolfgang Jeltsch (Aug 02 2023 at 19:26):Implicit conversions considered harmful?
Mathias Fleury (Aug 02 2023 at 19:28):well there can be very useful
Mathias Fleury (Aug 02 2023 at 19:29):it just took me a while to figure out how the typing and the implicit conversion was hurting me in that case
Last updated: May 02 2024 at 01:06 UTC