Mark Wassell (Dec 22 2020 at 07:47): Mark Wassell (Dec 22 2020 at 07:47):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?
Manuel Eberl (Dec 22 2020 at 08:53):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 21 2024 at 16:20 UTC