@edwinbrady I'd need my universal quantifier in Idris to go further in my experiment, any seconds to allocate to me? :p
-
-
@edwinbrady As you can't find funny jokes about proofs, at least you can find hilarious ones about XML ;) -
@mandubian I tried it. The reason for the error is that the 'm' in each FV is a different one, since what you have *is* a real forall… - 6 more replies
New conversation -
-
-
@edwinbrady@mandubian you let them bully you into docbook? We had them considering accepting our LaTeX until preprint. -
@bitemyapp@mandubian there's some advantages to their docbook style, so I didn't fight. At least it isn't Word. And I have vim macros :) - 10 more replies
New conversation -
-
-
@edwinbrady@mandubian you teach JS at St. Andrews? -
@bitemyapp@mandubian we teach all sorts, depending on the degree they're doing. This is for a masters in IT and Management.
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.