I am trying to understand options in Isabelle (2020), and couldn't understand why some simple expressions of option do not compute or simplify as expected.
For example, I'd expect that
value "some (1::nat)"
should return an "nat option" type, yet, it returns an unspecified type:
"some 1"
:: "'a
More over, from the type signature, I'd expect the the function the return the value "inside" the option, so that "the (some (1::nat))" is just (1::nat).
However,
value "the (some (1::nat))"
returns a seemingly not very useful type:
"the (some 1)"
:: "'a"
, which isn't nat. Then the result isn't very useful, e.g.
value "the (some (1::nat)) + 2"
returns
"the (some 1) + (1 + 1)"
:: "'a"
(I expected the result to be "3::nat")
Is this by design or am I missing something about the, or how options simplify/compute in Isabelle?
( I have no prior knowledge about Isabelle options, and I am just assuming it's similar to Haskell's Maybe. )
A C-click on the shows that the definition is:
datatype 'a option =
None
| Some (the: 'a)
It is Some, not some.
There is a hint to see that some is not defined: the color is not the same as the color from the.