Andrej Bauer

And what happens to non-terminating computations? Don't they generate rather large values in the free monad? Ok, you said it was inefficient...

I think there's general leg pulling going on here. Let's just get back to coding ;-)

Hi, sorry for not noticing this PR earlier. What do you mean by "merge" Cauchy and Dedekind reals? Which lemma in the PR expresses this?

@zigaLuksic : it's not that much work. It sounds like half an hour of work, so it's probably about two hours of work.

I think this issue presents a very realistic and nice test case for effects: what is the Correct Way of working with files?

1. Rather than posting a lot of code in the comments, you should fork the repository, commit your code, and then we can look at your commit log. Now we...

But other than that, great work :-)

Are you talking about coqide compiled from HoTT/coq, or about hoqide?

> Both have the same behavior. Therefore it is a Coq problem. You are _sure_ you're trying to run just standard coqide, and not something related to HoTT? > Incidentally,...

Obviously they should produce vanilla HTML and use CSS for the looks. I remember being annoyed by coqdoc in the past for being so outdated.