Andrej Bauer
Andrej Bauer
Correct me if I am wrong, but aren't we doing the case of HIT which can be factored out into an ordinary inductive type followed by a coequalizer? If not,...
What is the purpose of separating the recursive and nonrecursive constructors? This should not be necessary. Also, where is the notion of "nonrecursive" and "recursive" constructor defined?
Speaking intuitionistically, there are three kinds of reals, depening on how we phrase completeness: * **Cauchy reals:** archimedean ordered field in which every Cauchy sequence has a limit * **Dedekind...
``` * In Example 1.17, the definition of [[op_i]] is correct just for operations of arity 1. (Also in this definition, L and M are swapped from their order in...
``` p. 3, Ex 1.3. "...the second one in x, y, and the last two in x." should probably be, "...the second one x, y, and the last two x."...
Example 2.7 should state that we perform an induction on the tree in order to get it into the desired form.
Žiga Lukšič [2:53 PM] Živjo, trenutno prebiram tvoj 'whats algebraic about algebraic effects', na strani 16 je pri tretji enačbi `update` kjer domnevam, da je mišljen `put`? Žiga Lukšič [3:43...
Why do we have `eval` functions in `eval.ml` as well as in `first_order.ml`?
It seems that `eventual_period` in `unary_invariant` and `binary_invariant` is needlessly quadratic time. If we keep track of _when_ we saw each element, then when an element re-appears, we will instantly...
Abstract sytnax does not keep the source code locations. This is bad because error reporting cannot give information about where an error occurred.