Email Gateway (Aug 19 2022 at 13:56): Email Gateway (Aug 19 2022 at 13:56):From: Gottfried Barrow <igbi@gmx.com>
Hi,
I probably wouldn't report this, since I've mainly interpreted
exceptions as error messages without a nice interface, but I mentioned
an exception in the past, and then Ondrej Kuncar implemented an
important change.
I moved on to a different solution, but what's below represents what I
was trying, and it looks like it could be useful if it did work.
My first example is a function of type "nat list => nat", and it shows I
can match on a 0-ary constructor in a list.
My second example is a function of type "(nat => nat) list => nat", and
it shows that when I try to match on Suc, it causes an exception.
Here are the examples:
fun nat_con_0_no_error :: "nat list => nat" where
"nat_con_0_no_error [0] = 0"
fun nat_con_Suc_error :: "(nat => nat) list => nat" where
"nat_con_Suc_error [Suc] = 0"
(* OUTPUT: exception Option raised (line 81 of "General/basics.ML") *)
Thanks,
GB
Email Gateway (Aug 19 2022 at 13:56):From: Lars Noschinski <noschinl@in.tum.de>
This fails as functions are not a datatype and "Suc" is not a
constructor of "nat => nat".
-- Lars
signature.asc
Email Gateway (Aug 19 2022 at 13:56):From: Gottfried Barrow <igbi@gmx.com>
Lars,
Thanks. I knew "fun" requires a constructor for pattern matching,
because the standard error message tells me that a lot.
But I was foggy on the rules for nesting constructors, where I wasn't
even clear on it enough to be thinking "nested constructors".
Thanks again,
GB
Last updated: May 06 2024 at 20:16 UTC