Stream: General

Topic: Converse relation notation

view this post on Zulip Gergely Buday (Jan 30 2026 at 09:45):

For the expression 

term "conversep R"

I got
R superscript {-1 -1}

I expected one superscript -1, not two. Is this a bug?

This is in Isabelle2025-2.

view this post on Zulip Maximilian Schäffeler (Jan 30 2026 at 10:38):

The set relation version converse comes with the single subscript notation. The notation for conversep is consistent with other operations on relations, e.g. O vs. OO for composition.

view this post on Zulip Gergely Buday (Jan 30 2026 at 10:38):

I see, thanks

Last updated: Feb 06 2026 at 20:37 UTC