[Agda-dev] A tutorial on inference in Agda

[Nils Anders Danielsson]

On 2020-10-26 03:03, Roman wrote:
> Does Agda support generating an HTML page (with all the coloring) from
> an Agda file when that file contains warnings, unresolved metas etc?

I tried the following code:

   {-# OPTIONS --allow-unsolved-metas #-}

   A : Set
   A = _
   A = _

The code is not highlighted in quite the same way as in the Emacs mode
(at least in the browser that I tried): the final underscore gets the
dead code highlighting, rather than the one for unsolved meta-variables.
I could fix this by reordering some lines in Agda.css, but I don't know
if the CSS standard requires browsers to respect the ordering of lines
in this way.

> And is there a flag to make Agda accept ill-typed code, show a warning
> and proceed with type checking?

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

-- 
/NAD