Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Ignored {} sort constraint when using undersco...

Email Gateway (Jan 27 2026 at 10:41):

From: Kevin Kappelmann <cl-isabelle-users@lists.cam.ac.uk>

Hi everyone,

It seems that "{}" sort constraints are not respected when using
underscore type patterns. Examples:

theory Scratch
   imports Main
begin
declare[[show_sorts]]
term "foo :: 'a :: {}" (*check output window: "{}" sort constraint*)
term "foo :: _ :: {}" (*got "type" sort constraint, but expected "{}"*)
term "foo :: _ :: ord" (*"ord" sort constraint*)
definition "foo (x :: 'a :: {}) ≡ x" (*"{}" sort constraint*)
definition "bar (x :: _ :: {}) ≡ x" (*"type" sort constraint*)
end

I am using the latest Isabelle development version.

Best wishes,

Kevin

Email Gateway (Jan 27 2026 at 10:50):

From: Makarius <makarius@sketis.net>

On 27/01/2026 11:41, Kevin Kappelmann (via cl-isabelle-users Mailing List) wrote:

I am using the latest Isabelle development version.

So which one is it, actually? "Latest" is always many weeks months ago.

Makarius

Email Gateway (Jan 27 2026 at 10:54):

From: Kevin Kappelmann <cl-isabelle-users@lists.cam.ac.uk>

changeset: 16365:135f032810f4
date: Mon Jan 26 21:01:41 2026 +0000

Best wishes,

Kevin

On 27.01.26 11:49, Makarius wrote:

On 27/01/2026 11:41, Kevin Kappelmann (via cl-isabelle-users Mailing
List) wrote:

I am using the latest Isabelle development version.

So which one is it, actually? "Latest" is always many weeks months ago.

Makarius

Last updated: Jan 31 2026 at 12:53 UTC