I would like to be able to do things like
value "10"
without have to add type annotations. Is there something that I can write that will tell Isabelle that all numeric literals have type nat. Is there a context I should be in?
Hm, the only ways I can think of are either making a modified version of the value
command or using something like an extra checking phase. One could add extra constraints to the numeral
function, but that is a bad idea because that is a global thing (i.e. cannot be constrained to a local context).
Last updated: Dec 07 2024 at 16:22 UTC