I am trying to write a quick abbreviation, as follows:
abbreviation threshold :: "nat ⇒ rat" where "threshold n ≡ of_int (floor ((of_nat n) / 2) + 1)"
However, that already gives me a warning which I don't understand:
Additional type variable(s) in specification of "threshold": 'a, since I have no type variables in that abbreviation?
Then, using that abbreviation...
definition my_def :: "bool" where "my_def ≡ ∀p. 123 > threshold (length p)"
...I get an error:
Operator: threshold :: ??'a itself ⇒ nat ⇒ rat Operand: length p :: nat
And I don't understand where
??'a itself comes from.
The warning tells you that some constants in your abbreviation can have multiple types, so they've been assigned a type variable
If you ctrl+hover over
2, you'll see that their inferred types are
'a => int,
nat => 'a and
Ah, yeah disambiguating with
(of_nat n)::rat helped. Glad the solution was so simple, thank you!
you could also use the name
Ahhhh, TIL you can ctrl-hover!
n div 2, which is floored divison
Oh yeah that simplifies it further, thank you :)
When you do want to use
floor, there's the syntax
⌊a⌋ (which you can type with
.] and selecting between floor and ceiling in the autocompletion menu)
The reason your
threshold abbreviation got a
'a itself parameter is that the actual value of the abbreviation depends on which type you choose. You can think of
'a itself as a witness that tells you which type to actually use
so, if you actually wanted to parametrize your
threshold by what type is used for intermediate computation, you could invoke it with
threshold TYPE(rat) (length p)
Huh, that is neat actually, but not necessary for what I'm doing.
Yeah you basically almost never want that.
'a itself is a singleton type, just so that you've heard the term. (They are also used in functional programming)
Last updated: Dec 07 2023 at 20:16 UTC