John Hughes (Oct 27 2025 at 22:59): John Hughes (Oct 27 2025 at 22:59):I've got a function "perspectivity" that takes 3 arguments -- a point and two lines. I've made a fake version here that takes 3 ints so that I don't have to include other definitions.
Perspectivity is denoted like this
image.png in the book we're working from, and in an attempt to capture something that that notation, I developed the notation below. Yes, in my case the point sits below instead of above the dash, and there no little wedge, but it's close enough:
fun perspectivity::"int ⇒ int ⇒ int ⇒ int" where
"perspectivity l1 P l2 = 0"
notation perspectivity (‹( _/ -⇩_-/ _)› 10)
term "perspectivity l1 P l2"
The result looks like this:
image.png
Unfortunately, we'd really like to have this be the notation for "perspectivity P l1 l2", because in the actual definition, the point comes first (and this is 'natural' for various other parts of the development). Is there any way to refer to the arguments when writing mixfix so that the second arg can come first in the notation, etc?
I assume not, or my search through various theory files in the sources might have revealed it, but if someone can confirm that it's hopeless, or tell me how to do it if it's possible, that'd be great.
Kevin Kappelmann (Oct 28 2025 at 06:57):You can add an abbreviation for the infix notation:
abbreviation "perspectivity_infix P l1 ≡ perspectivity l1 P"
notation perspectivity_infix (...)
I also do that in the AFP, e.g. here
John Hughes (Oct 29 2025 at 01:21):Excellent solution -- thanks very much!
Last updated: Nov 13 2025 at 04:27 UTC