Stream: General

Topic: Case expression vs pattern matching in a locale

Gergely Buday (Feb 21 2025 at 10:58):

I am to define a function in a locale that uses a fixed function parameter of the locale:

theory LocaleFunction

imports Main

begin

datatype 'a bar = Baz | Bar 'a

locale simple =
  fixes a :: "'a"
and foo :: "'a ⇒ nat"
begin

fun foobar :: "'a bar ⇒ nat"
  where
  "foobar x = (case x of Baz ⇒ 0 | (Bar a) ⇒ foo a)"

fun barfoo :: "'a bar ⇒ nat"
  where
  "barfoo Baz = 0"
| "barfoo (Bar a) = foo a"

Now, foobar goes well, with a case expression, but barfoo with a pattern matching does not go through, it gives this error message:

Malformed definition:
Non-constructor pattern not allowed in sequential mode.
barfoo (Bar a) = foo a

I wonder about this, as (Bar a) seems to be a constructor pattern for me.

What does cause this problem?

terru (Feb 21 2025 at 11:03):

the name a in the pattern clashes with the a fixed in the locale (and it's not a pattern if it contains an existing constant — you also can't use Bar foobar as a pattern). If you rename it, this works

Last updated: Feb 28 2025 at 08:24 UTC