Stream: Beginner Questions

Topic: Numeric literals


view this post on Zulip 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?

view this post on Zulip 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: Sep 25 2021 at 09:17 UTC