[Agda-dev] A tutorial on inference in Agda

[Roman]

Nils, I tried using the pragma and calling `agda --html
UnificationInAgda.lagda.md`, but that gave me a ton of messages like

Refusing to invert pattern matching of _+_ because the maximum
depth (50) has been reached. Most likely this means you have an
unsatisfiable constraint, but it could also mean that you need to
increase the maximum depth using the flag --inversion-max-depth=N
when checking that the inferred type of an application
  Vec ℕ 2
matches the expected type
  Vec ℕ (_n_944 + 1)
Incomplete pattern matching for UnificationInAgda.Div-v2.with-1208.
Missing cases:
  secondNumber-direct | []
  secondNumber-direct | x ∷ []
when checking the definition of UnificationInAgda.Div-v2.with-1208
Failed to solve the following constraints:
  ℕ → ℕ → ℕ =< ToFunᵥ _As_1575 _B_1574
  ℕ =< ToFun _xs_1173 _B_1147

and no HTML was generated. Is that the expected and desired behavior?

> No (see https://github.com/agda/agda/issues/2114).

Thanks, left a comment there.