4 ms·
Really cool, but I am assuming printf only works for values which are determined at compile time?
by wz1000 12y ago
Really cool, but I am assuming printf only works for values which are determined at compile time?
- chriswarbo 12y agoAFAIK the value of the formatting string needs to be known at compile time. Only the types of the rest need to be known. Actually, since it's dependently typed, we don't actually need to know the value of the formatting string; we just need a proof that the formatting string will match the other values. The easiest way to do this is to know what the string is, but we could also, for example, get these values from a function, then prove that the function produces matching values.