Stream: Beginner Questions

Topic: Type Checking Error: Matrices

Kubra (Sep 26 2023 at 18:42):

Dear all,

I am trying to construct a 4 by 4 matrix using the 3 by 3 matrix in HMA library as follows:

typeerror_matrix4x4.png

I got type error as you can see in the screenshot. How can I fix this problem?

Thanks in advance,
Kubra

Wenda Li (Sep 26 2023 at 19:45):

The error is because indices of A are of type 3 and the bounded variables i and j are of type 4, and Isabelle does not know how to automatically convert from this one type to another. We can perhaps do this conversion manually, but it is not immediately to me how to do it.

Nevertheless, given the inflexibility of the HOL type system, my personal choice would be to avoid encoding matrix dimension into types. In particular, the two-dimensional matrix type 'a mat from the AFP entry Jordan_Normal_Form is much easier to work with than the vec encoded matrices, e.g., ((real, 'b) vec, 'c) vec.

Kubra (Oct 08 2023 at 22:56):

Thanks.

Last updated: Apr 28 2024 at 08:19 UTC