Email Gateway (Aug 22 2022 at 17:45): Email Gateway (Aug 22 2022 at 17:45):From: Anthony Bordg <bordg.anthony@gmail.com>
Dear all,
In the theory Matrix.thy available in the AFP entry "Matrices, Jordan
Normal Forms and Spectral Radius Theory" (authors: Rene Thiemann and
Akihisa Yamada), one can find the definition module_vec :: " 'a::
semiring_1 itself => nat => ('a,'a vec) module" (in section 4.1 Vectors).
I would like to instantiate module_vec with complex, the type of complex
numbers, as its first argument, but if I do that I get the error "Extra
variables on rhs: "complex" ". So, complex does not seem to be recognized
as a valid first argument. So, I tried something like "module_vec (complex
:: semiring_1 itself) n", where n is a natural number, but then I got the
following error "Undefined type name "semiring_1" ".
Can someone tell me how I can instantiate module_vec with the type of
complex numbers as its first argument ?
Best regards
Anthony
Email Gateway (Aug 22 2022 at 17:45):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Anthony,
The first argument is a type token, i.e. a type reified as a value. The right syntax for that is TYPE(complex).
Hope this helps,
Andreas
Last updated: Nov 21 2024 at 12:39 UTC