I would like to be able to do things like
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: Sep 25 2021 at 09:17 UTC