Email Gateway (Aug 22 2022 at 20:29): Email Gateway (Aug 22 2022 at 20:29):From: José Manuel Rodríguez Caballero <josephcmac@gmail.com>
Hello,
In [1], I defined the (algebraic) tensor product of two types
'a::complex_vector_space" and 'b::complex_vector_space, denoted (('a, 'b)
atensor)::complex_vector_space. I prefer to use the notation 'a ⊗⇩a 'b
instead (the subscript "a" is for "algebraic", because there is another
tensor product with another subscript). This notation was implemented as
type_notation (xsymbols)
atensor ("(_ ⊗⇩a/ _)" [21, 20] 20)
type_notation (HTML output)
atensor ("(_ ⊗⇩a/ _)" [21, 20] 20)
Nevertheless, when I invoke "sketch", in the automatically generated sketch
of the proof the notation ('a, 'b) atensor appears.
How could I guarantee that sketch of the proof will be written using the
notation " 'a ⊗⇩a 'b " in place of " ('a, 'b) atensor "?
Kind regards,
José M.
References:
[1]
https://github.com/dominique-unruh/bounded-operators/blob/master/Tensor_Product.thy
Last updated: Apr 25 2024 at 20:15 UTC