Re: [isabelle] Error: Non-constructor pattern not allowed in sequential mode
record Foo =
x :: "nat"
y :: "nat"
fun bar :: "Foo => nat => nat"
"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
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...
This archive was generated by a fusion of
Pipermail (Mailman edition) and