(Minor) Suggestion for Definition of dfold

Skip to first unread message

Pat the Builder

Dec 29, 2021, 9:06:20 AM12/29/21
to Clash - Hardware Description Language

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
        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)


Leon Schoorl

Jan 11, 2022, 8:48:09 AM1/11/22
to clash-l...@googlegroups.com
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.


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.
Reply all
Reply to author
0 new messages