[Agda-dev] A tutorial on inference in Agda

[Nils Anders Danielsson]

On 2020-11-02 23:21, Roman wrote:
> Nils, I tried using the pragma and calling `agda --html
> UnificationInAgda.lagda.md`, but that gave me a ton of messages like
> […] and no HTML was generated. Is that the expected and desired
> behavior?

If you add

   {-# NON_COVERING #-}

right before secondNumber-direct, then you get HTML output. I think that
Agda refuses to generate output if there are any non-benign warnings.
You can use

   agda --help=warning

to see which warnings are benign and which are not.

-- 
/NAD