In the code you’ve shown:
O
has typezero
.K
takes aneg
as argument to construct aneg
.O
is not aneg
.- Therefore,
K O
is not a valid expression. - Moreover, you can’t write any instance of
pos
orneg
, because both inductive definitions lack a base case. A positive number must be “either one, or some positive number plus one”; Similarly, a negative number must be “either negative one, or some negative number minus one”.
You can define integers as “zero, positive, or negative”:
Inductive pos :=
| One
| S (n : pos).
Variant Z' :=
| Z0' (* zero *)
| Zpos' (n : pos) (* positive [n] *)
| Zneg' (n : pos). (* negative [n] *)
If you prefer asking (and responded) in Chinese, please feel free to post under the other thread you created: