Stream: General

Topic: Dropping global mixfix syntax

view this post on Zulip Jakub Kądziołka (May 29 2021 at 22:13):

I am using the following code to define a function with mixfix syntax that depends on a context's parameter:

context
  fixes a :: real
  assumes "a > 0"
begin

fun x :: "nat ⇒ real" ("x⇘_⇙") where
  "x⇘0⇙ = 0" |
  "x⇘Suc n⇙ = a + x⇘n⇙⇧2"

This works, except for the following warning: Dropping global mixfix syntax: "x" (‹x⇘_⇙›) . Does this indicate that I'm doing something wrong? Can I silence it by doing this differently?

view this post on Zulip Mathias Fleury (May 30 2021 at 12:26):

If I got https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-June/msg00034.html correctly, you can ignore the warning.

Last updated: Oct 31 2025 at 01:43 UTC