Search code examples
isabelle

Function definition with one argument as index

This question is somewhat related to function with index

Imagine the definition of the function is

definition myf :: "nat => nat => nat" where
  "myf n a = n * a"

and I want to use a more readable abbreviation

"f<sub>n</sub> a"

instead of

"myf n a"

I have tried

definition myf :: "nat => nat => nat" **("f<sub>_</sub> _" [90])** where
  "f<sub>n</sub> a = n * a"

and I get the error Head of definition "fn" differs from declaration "myf".

How am I supposed to write the prefix s.t. it gives me what I am looking for?

Thank you in advance

Solution

  • Subscripts that span a region of text can be marked up with \<^bsub>...\<^esub> (or, equivalently, ⇘...⇙). Therefore, your definition should be as follows:

    definition myf :: "nat => nat => nat" ("f⇘_⇙") where
  "f⇘n⇙ a = n * a"

    For further information see Appendix B in The Isabelle/Isar Reference Manual.