Theory Shows_Literal_Matrix
theory Shows_Literal_Matrix
imports
Jordan_Normal_Form.Matrix
Show.Shows_Literal
begin
subsection ‹For the @{class showl}-class›
instantiation Matrix.vec :: (showl)showl begin
definition showsl_vec :: "'a Matrix.vec ⇒ showsl" where
"showsl_vec v ≡ showsl_list (list_of_vec v)"
definition "showsl_list (xs :: 'a Matrix.vec list) = default_showsl_list showsl xs"
instance ..
end
instantiation mat :: (showl)showl begin
definition showsl_mat :: "'a Matrix.mat ⇒ showsl" where
"showsl_mat a ≡ default_showsl_list id (map showsl_list (mat_to_list a))"
definition "showsl_list (xs :: 'a Matrix.mat list) = default_showsl_list showsl xs"
instance ..
end
value "showsl (one_mat 3 :: nat mat) (STR '' is the identity matrix of dimension 3'')"
end