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:

  fixes a :: real
  assumes "a > 0"

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 correctly, you can ignore the warning.

Last updated: Aug 15 2022 at 02:13 UTC