[isabelle] Error: Non-constructor pattern not allowed in sequential mode
I just got this error and I don't know how to work around. The code is like
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".
How can we use record patterns in functions like the one above?
This archive was generated by a fusion of
Pipermail (Mailman edition) and