From: Rebecca Ghidini <ghidini@in.tum.de>
Hello,
I'm trying to write a function which uses pattern matching on an
extended record.
For example, if I define the following record:
record normal_record =
t1 :: nat
t2 :: nat
I can define functions with pattern matching on the fields of the
record:
fun test1 :: "normal_record => nat"
where
"test1 ((|t1 = a, t2 = b|)) = b"
Then I define an extended record:
record extended_record = normal_record +
t3 :: nat
But when I try to define a function in the same way as before, I get an
error:
fun test2 :: "extended_record => nat"
where
"test2 ((|t1 = a, t2 = b, t3 = c|)) = b + c"
This is the error:
exception THM 0 raised (line 755 of "drule.ML"):
infer_instantiate_types: type ?'z extended_record_scheme of variable
?r
cannot be unified with type (|t3 :: nat|) of term _av4
(⋀t1 t2 t3 more. ?r = (|t1 = t1, t2 = t2, t3 = t3, … = more|) ⟹ ?C) ⟹
?C
I tried to define the function in different ways, for example using "'a
extended_record_scheme"
instead of "extended_record" or adding the "more" field explicitly, but
I always get the same error.
I also tried pattern matching with "case … of", but it doesn't work,
because record is not a datatype constructor.
Obviously I could define the function like this:
fun test4 :: "extended_record => nat"
where
"test4 rec = t2 rec + t3 rec"
But given that I am working with larger records and more complicated
functions, I was wondering if there is a more
elegant way to write this function, by using pattern matching.
Thank you,
Rebecca
Last updated: Jan 04 2025 at 20:18 UTC