Email Gateway (Aug 18 2022 at 17:53): Email Gateway (Aug 18 2022 at 17:53):From: Anh Le <anhlevn@cims.nyu.edu>
Hi everyone,
I just got this error and I don't know how to work around. The code is like
(not exactly):
record Foo =
x :: "nat"
y :: "nat"
fun bar :: "Foo => nat => nat"
where
"bar (| x = n1, y = n2|) z = compute n1 n2 z"
But it doesn't allow the record pattern there. I got the error
"Non-constructor pattern not allowed in sequential mode".
How can we use record patterns in functions like the one above?
Thank you
Anh
Email Gateway (Aug 18 2022 at 17:53):From: Alexander Krauss <krauss@in.tum.de>
Hi Anh,
record Foo =
x :: "nat"
y :: "nat"fun bar :: "Foo => nat => nat"
where
"bar (| x = n1, y = n2|) z = compute n1 n2 z"But it doesn't allow the record pattern there. I got the error
"Non-constructor pattern not allowed in sequential mode".
The fun command does not support record patterns, just datatype
constructors (even though records are much like datatypes).
How can we use record patterns in functions like the one above?
There are two possibilities: Either you use functions general patterns,
which gives you some manual (but trivial) proving work to do; see
HOL/ex/Fundefs.thy for an example. Or, which is probably easier, you use
the "rep_datatype" command to instruct the system to regard the record
type you defined as a datatype: After the record definition, do
rep_datatype Foo_ext
by (fact Foo.ext_induct) (fact Foo.ext_inject)
Then, the function definition works out of the box.
Someone who knows more about records can probably explain why this
declaration isn't issued internally by default...
Alex
Email Gateway (Aug 18 2022 at 17:53):From: Makarius <makarius@sketis.net>
Strictly speaking, this exposes implementation details of version 12 of
the record package (or is it version 17). It should work for now, but
nobody can say when there will be the next change in the internal
representation.
Makarius
Last updated: Apr 23 2024 at 20:15 UTC