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?
If I got https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-June/msg00034.html correctly, you can ignore the warning.
Last updated: Dec 07 2023 at 08:19 UTC