[Agda] Impossible proofs about where blocks?

[Nils Anders Danielsson]

On 2011-06-16 01:26, Daniel Peebles wrote:
> Note that it will not proceed in normalizing the goal type unless I
> can match on the result of the expression after the pipe.
> Unfortunately, said expression lives within a where block in a module
> that's out of my control, so I can't see it at all, to proceed on the
> proof. As far as I can understand, assuming there aren't completely
> different approaches to the proof, this makes my proof actually
> impossible. Am I correct?

The type of toDigits b n specifies that the result is a list of digits
ds, in base b, with the property that fromDigits ds ≡ n. Do you really
need to know the implementation of toDigits?

-- 
/NAD