[Agda] _ synthax

Nils Anders Danielsson nad at chalmers.se
Tue Feb 22 11:20:41 CET 2011


On 2011-02-22 08:13, Permjacov Evgeniy wrote:
> What meaning (both from user and typechecker perspective) does synthax
> "Set _" have ? If I understand correctly, it is instruction to infer
> level from context, but how it is done ?

Using unification, extended in an ad-hoc and buggy way.

-- 
/NAD


More information about the Agda mailing list