(Minor) Suggestion for Definition of dfold

[Pat the Builder]

Hello,

The cast `:: Vec z a` in the last equation of `go` of `dfold` (see below) is confusing. It took a few minutes before I understood it's not needed. IMO  `go s (y `Cons` ys)` would be a bit clearer.

    dfold _ f z xs = go (snatProxy (asNatProxy xs)) xs
      where
        go :: SNat n -> Vec n a -> (p @@ n)
        go _ Nil                        = z
        go s (y `Cons` (ys :: Vec z a)) = -- Use `go s (y `Cons` ys) = ` ?
          let s' = s `subSNat` d1
          in  f s' y (go s' ys)

/Paddy

[Leon Schoorl]

You're right, that is confusing and unnecessary.

Especially since there is also a term variable called z.

That type variable z was used in the past, but hasn't been used for a long time now.

I'll remove it.

Leon

Op wo 29 dec. 2021 om 15:06 schreef Pat the Builder <paddythep...@gmail.com>:

--
You received this message because you are subscribed to the Google Groups "Clash - Hardware Description Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to clash-languag...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/clash-language/374a76ac-b349-41bc-988f-4dccef67feb5n%40googlegroups.com.