[Agda] syntactic sugar parameters

Nils Anders Danielsson nad at cse.gu.se
Fri Dec 6 10:09:40 CET 2019


On 2019-12-05 13:05, Herminie Pagel wrote:
> What kind of syntactic sugar is making agda understand sample-pf
> without explicitly telling Assume its parameters in the first place?

Agda uses unification to infer these arguments. Ulf Norell's PhD thesis
discusses this topic (but Agda has evolved quite a bit since the thesis
was published).

-- 
/NAD


More information about the Agda mailing list