gistfile1.idr

-- error: expected: "{",
--    function declaration
--  | M = MD5 (zipWith (+) [A, B, C, D] (loop 64 [A, B, C, D])) 


updateMD5Context : MessageDigest5 -> Bits 512 -> MessageDigest5
updateMD5Context (MD5 [A, B, C, D]) chunk with (the (Vect 16 (Bits 32)) (partition chunk))
  | M = MD5 (zipWith (+) [A, B, C, D] (loop 64 [A, B, C, D]))
  where loop : Fin 65 -> Vect 4 (Bits 32) -> Vect 4 (Bits 32)
        loop fZ     context      = context
        loop (fS x) [A, B, C, D] =
            let i = (the (Fin 64) last) `Prelude.Fin.(-)` x
            in let iNat = finToNat i
               in let (F, g) =
                        if iNat < 16
                        then ((B `and` C) `or` (complement B `and` D),
                              iNat `tightmod` 16)
                        else if iNat < 32
                             then ((D `and` B) `or` (complement D `and` C),
                                   (iNat*5 + 1) `tightmod` 16)
                             else if iNat < 48
                                  then (B `xor` (C `xor` D),
                                        (iNat*3 + 5) `tightmod` 16)
                                  else (C `xor` (B `or` complement D),
                                        (iNat*7) `tightmod` 16)
                  in loop (weaken x)
                          [C,
                           B,
                           B + rotateLeft (A `plus` F `plus` index i K `plus` index g M)
                                          (index i s),
                           D]

I got this to load:

updateMD5Context : MessageDigest5 -> Bits 512 -> MessageDigest5
updateMD5Context (MD5 [A, B, C, D]) chunk with (the (Vect 16 (Bits 32)) (partition chunk))
  | M = MD5 (zipWith plus [A, B, C, D] (loop 64 [A, B, C, D]))
  where loop : Fin 65 -> Vect 4 (Bits 32) -> Vect 4 (Bits 32)
        loop _     context      = context