[Agda] Unification assumes injective postulates?

Nils Anders Danielsson nad at chalmers.se
Thu Nov 22 10:42:04 CET 2012

On 2012-11-16 22:30, Jan Malakhovski wrote:
> "Besides even if we treated postulates like parameters things might
> break once you start replacing them with actual definitions, since the
> metavariable solver will behave differently."
> What might brake? It's fine if it's only a bunch of unsolved implicit
> arguments. Might it stop type-checking completely?

AFAIK unsolved meta-variables can, in some cases, lead to a type error.


More information about the Agda mailing list