[Agda] _ synthax

Permjacov Evgeniy permeakra at gmail.com
Tue Feb 22 08:13:38 CET 2011


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 ?


More information about the Agda mailing list