Hello,
when `:N` is an infinite type, `dimindex(:N)` is by definition 1.
Then, if either `:M` or `:N` is infinite, we have
dimindex(:M+N) = 1
while
dimindex(:M) + dimindex(:N) >= 2
It follows that your relation
dimindex (:M+N) = dimindex(:M)+dimindex(:N)
holds only if `:M` and `:N` are both finite types.
I believe that the type `:(M,N)finite_sum` has been introduced precisely to
get around this problem.
Marco
2018-03-16 2:49 GMT+01:00 liliminga <lilimi...@126.com>:
>
> Hi, everyone.
> I know the type :(M,N)finite_sum in library "Definition of finite
> Cartesian product types". What is the difference between (:M+N) and
> :(M,N)finite_sum? Is there the theorem |- dimindex (:M+N) =
> dimindex(:M)+dimindex(:N) in the existing library?
> Thank you very much.
> Best regards,
> Liming
>
> 2018-03-16
> ------------------------------
> liliminga
>
>
>
>
> ------------------------------------------------------------
> ------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
